Step | Hyp | Ref
| Expression |
1 | | txcnpi.3 |
. . 3
⊢ (𝜑 → 𝐹 ∈ (((𝐽 ×t 𝐾) CnP 𝐿)‘〈𝐴, 𝐵〉)) |
2 | | txcnpi.4 |
. . 3
⊢ (𝜑 → 𝑈 ∈ 𝐿) |
3 | | df-ov 6552 |
. . . 4
⊢ (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) |
4 | | txcnpi.7 |
. . . 4
⊢ (𝜑 → (𝐴𝐹𝐵) ∈ 𝑈) |
5 | 3, 4 | syl5eqelr 2693 |
. . 3
⊢ (𝜑 → (𝐹‘〈𝐴, 𝐵〉) ∈ 𝑈) |
6 | | cnpimaex 20870 |
. . 3
⊢ ((𝐹 ∈ (((𝐽 ×t 𝐾) CnP 𝐿)‘〈𝐴, 𝐵〉) ∧ 𝑈 ∈ 𝐿 ∧ (𝐹‘〈𝐴, 𝐵〉) ∈ 𝑈) → ∃𝑤 ∈ (𝐽 ×t 𝐾)(〈𝐴, 𝐵〉 ∈ 𝑤 ∧ (𝐹 “ 𝑤) ⊆ 𝑈)) |
7 | 1, 2, 5, 6 | syl3anc 1318 |
. 2
⊢ (𝜑 → ∃𝑤 ∈ (𝐽 ×t 𝐾)(〈𝐴, 𝐵〉 ∈ 𝑤 ∧ (𝐹 “ 𝑤) ⊆ 𝑈)) |
8 | | eqid 2610 |
. . . . . . . . . 10
⊢ ∪ (𝐽
×t 𝐾) =
∪ (𝐽 ×t 𝐾) |
9 | | eqid 2610 |
. . . . . . . . . 10
⊢ ∪ 𝐿 =
∪ 𝐿 |
10 | 8, 9 | cnpf 20861 |
. . . . . . . . 9
⊢ (𝐹 ∈ (((𝐽 ×t 𝐾) CnP 𝐿)‘〈𝐴, 𝐵〉) → 𝐹:∪ (𝐽 ×t 𝐾)⟶∪ 𝐿) |
11 | 1, 10 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:∪ (𝐽 ×t 𝐾)⟶∪ 𝐿) |
12 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐽 ×t 𝐾)) → 𝐹:∪ (𝐽 ×t 𝐾)⟶∪ 𝐿) |
13 | | ffun 5961 |
. . . . . . 7
⊢ (𝐹:∪
(𝐽 ×t
𝐾)⟶∪ 𝐿
→ Fun 𝐹) |
14 | 12, 13 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐽 ×t 𝐾)) → Fun 𝐹) |
15 | | elssuni 4403 |
. . . . . . 7
⊢ (𝑤 ∈ (𝐽 ×t 𝐾) → 𝑤 ⊆ ∪ (𝐽 ×t 𝐾)) |
16 | | fdm 5964 |
. . . . . . . . . 10
⊢ (𝐹:∪
(𝐽 ×t
𝐾)⟶∪ 𝐿
→ dom 𝐹 = ∪ (𝐽
×t 𝐾)) |
17 | 11, 16 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = ∪ (𝐽 ×t 𝐾)) |
18 | 17 | sseq2d 3596 |
. . . . . . . 8
⊢ (𝜑 → (𝑤 ⊆ dom 𝐹 ↔ 𝑤 ⊆ ∪ (𝐽 ×t 𝐾))) |
19 | 18 | biimpar 501 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ⊆ ∪ (𝐽 ×t 𝐾)) → 𝑤 ⊆ dom 𝐹) |
20 | 15, 19 | sylan2 490 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐽 ×t 𝐾)) → 𝑤 ⊆ dom 𝐹) |
21 | | funimass3 6241 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ 𝑤 ⊆ dom 𝐹) → ((𝐹 “ 𝑤) ⊆ 𝑈 ↔ 𝑤 ⊆ (◡𝐹 “ 𝑈))) |
22 | 14, 20, 21 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐽 ×t 𝐾)) → ((𝐹 “ 𝑤) ⊆ 𝑈 ↔ 𝑤 ⊆ (◡𝐹 “ 𝑈))) |
23 | 22 | anbi2d 736 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐽 ×t 𝐾)) → ((〈𝐴, 𝐵〉 ∈ 𝑤 ∧ (𝐹 “ 𝑤) ⊆ 𝑈) ↔ (〈𝐴, 𝐵〉 ∈ 𝑤 ∧ 𝑤 ⊆ (◡𝐹 “ 𝑈)))) |
24 | | txcnpi.1 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
25 | | txcnpi.2 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
26 | | eltx 21181 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝑤 ∈ (𝐽 ×t 𝐾) ↔ ∀𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (𝑧 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤))) |
27 | 24, 25, 26 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝑤 ∈ (𝐽 ×t 𝐾) ↔ ∀𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (𝑧 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤))) |
28 | 27 | biimpa 500 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐽 ×t 𝐾)) → ∀𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (𝑧 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) |
29 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝐴, 𝐵〉 → (𝑧 ∈ (𝑢 × 𝑣) ↔ 〈𝐴, 𝐵〉 ∈ (𝑢 × 𝑣))) |
30 | 29 | anbi1d 737 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝐴, 𝐵〉 → ((𝑧 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤) ↔ (〈𝐴, 𝐵〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤))) |
31 | 30 | 2rexbidv 3039 |
. . . . . . . 8
⊢ (𝑧 = 〈𝐴, 𝐵〉 → (∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (𝑧 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤) ↔ ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (〈𝐴, 𝐵〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤))) |
32 | 31 | rspccv 3279 |
. . . . . . 7
⊢
(∀𝑧 ∈
𝑤 ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (𝑧 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤) → (〈𝐴, 𝐵〉 ∈ 𝑤 → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (〈𝐴, 𝐵〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤))) |
33 | | sstr2 3575 |
. . . . . . . . . . . . 13
⊢ ((𝑢 × 𝑣) ⊆ 𝑤 → (𝑤 ⊆ (◡𝐹 “ 𝑈) → (𝑢 × 𝑣) ⊆ (◡𝐹 “ 𝑈))) |
34 | 33 | com12 32 |
. . . . . . . . . . . 12
⊢ (𝑤 ⊆ (◡𝐹 “ 𝑈) → ((𝑢 × 𝑣) ⊆ 𝑤 → (𝑢 × 𝑣) ⊆ (◡𝐹 “ 𝑈))) |
35 | 34 | anim2d 587 |
. . . . . . . . . . 11
⊢ (𝑤 ⊆ (◡𝐹 “ 𝑈) → (((𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤) → ((𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣) ∧ (𝑢 × 𝑣) ⊆ (◡𝐹 “ 𝑈)))) |
36 | | opelxp 5070 |
. . . . . . . . . . . 12
⊢
(〈𝐴, 𝐵〉 ∈ (𝑢 × 𝑣) ↔ (𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣)) |
37 | 36 | anbi1i 727 |
. . . . . . . . . . 11
⊢
((〈𝐴, 𝐵〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤) ↔ ((𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) |
38 | | df-3an 1033 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐹 “ 𝑈)) ↔ ((𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣) ∧ (𝑢 × 𝑣) ⊆ (◡𝐹 “ 𝑈))) |
39 | 35, 37, 38 | 3imtr4g 284 |
. . . . . . . . . 10
⊢ (𝑤 ⊆ (◡𝐹 “ 𝑈) → ((〈𝐴, 𝐵〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤) → (𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐹 “ 𝑈)))) |
40 | 39 | reximdv 2999 |
. . . . . . . . 9
⊢ (𝑤 ⊆ (◡𝐹 “ 𝑈) → (∃𝑣 ∈ 𝐾 (〈𝐴, 𝐵〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤) → ∃𝑣 ∈ 𝐾 (𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐹 “ 𝑈)))) |
41 | 40 | reximdv 2999 |
. . . . . . . 8
⊢ (𝑤 ⊆ (◡𝐹 “ 𝑈) → (∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (〈𝐴, 𝐵〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐹 “ 𝑈)))) |
42 | 41 | com12 32 |
. . . . . . 7
⊢
(∃𝑢 ∈
𝐽 ∃𝑣 ∈ 𝐾 (〈𝐴, 𝐵〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤) → (𝑤 ⊆ (◡𝐹 “ 𝑈) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐹 “ 𝑈)))) |
43 | 32, 42 | syl6 34 |
. . . . . 6
⊢
(∀𝑧 ∈
𝑤 ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (𝑧 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤) → (〈𝐴, 𝐵〉 ∈ 𝑤 → (𝑤 ⊆ (◡𝐹 “ 𝑈) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐹 “ 𝑈))))) |
44 | 43 | impd 446 |
. . . . 5
⊢
(∀𝑧 ∈
𝑤 ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (𝑧 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤) → ((〈𝐴, 𝐵〉 ∈ 𝑤 ∧ 𝑤 ⊆ (◡𝐹 “ 𝑈)) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐹 “ 𝑈)))) |
45 | 28, 44 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐽 ×t 𝐾)) → ((〈𝐴, 𝐵〉 ∈ 𝑤 ∧ 𝑤 ⊆ (◡𝐹 “ 𝑈)) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐹 “ 𝑈)))) |
46 | 23, 45 | sylbid 229 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐽 ×t 𝐾)) → ((〈𝐴, 𝐵〉 ∈ 𝑤 ∧ (𝐹 “ 𝑤) ⊆ 𝑈) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐹 “ 𝑈)))) |
47 | 46 | rexlimdva 3013 |
. 2
⊢ (𝜑 → (∃𝑤 ∈ (𝐽 ×t 𝐾)(〈𝐴, 𝐵〉 ∈ 𝑤 ∧ (𝐹 “ 𝑤) ⊆ 𝑈) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐹 “ 𝑈)))) |
48 | 7, 47 | mpd 15 |
1
⊢ (𝜑 → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐹 “ 𝑈))) |