MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  txdis1cn Structured version   Visualization version   GIF version
Theorem txdis1cn 23555
Description: A function is jointly continuous on a discrete left topology iff it is continuous as a function of its right argument, for each fixed left value. (Contributed by Mario Carneiro, 19-Sep-2015.)
Hypotheses
Ref Expression
txdis1cn.x (πœ‘ β†’ 𝑋 ∈ 𝑉)
txdis1cn.j (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘Œ))
txdis1cn.k (πœ‘ β†’ 𝐾 ∈ Top)
txdis1cn.f (πœ‘ β†’ 𝐹 Fn (𝑋 Γ— π‘Œ))
txdis1cn.1 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
Assertion
Ref Expression
txdis1cn (πœ‘ β†’ 𝐹 ∈ ((𝒫 𝑋 Γ—t 𝐽) Cn 𝐾))
Distinct variable groups:   π‘₯,𝑦,𝐹   π‘₯,𝐽   π‘₯,𝑋,𝑦   π‘₯,𝐾,𝑦   πœ‘,π‘₯   π‘₯,π‘Œ,𝑦
Allowed substitution hints:   πœ‘(𝑦)   𝐽(𝑦)   𝑉(π‘₯,𝑦)
Proof of Theorem txdis1cn
Dummy variables π‘Ž 𝑏 π‘š 𝑛 𝑒 𝑣 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 txdis1cn.f . . 3 (πœ‘ β†’ 𝐹 Fn (𝑋 Γ— π‘Œ))
2 txdis1cn.j . . . . . . 7 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘Œ))
32adantr 479 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ 𝐽 ∈ (TopOnβ€˜π‘Œ))
4 txdis1cn.k . . . . . . . 8 (πœ‘ β†’ 𝐾 ∈ Top)
5 toptopon2 22836 . . . . . . . 8 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾))
64, 5sylib 217 . . . . . . 7 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾))
76adantr 479 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾))
8 txdis1cn.1 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
9 cnf2 23169 . . . . . 6 ((𝐽 ∈ (TopOnβ€˜π‘Œ) ∧ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾) ∧ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) ∈ (𝐽 Cn 𝐾)) β†’ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)):π‘ŒβŸΆβˆͺ 𝐾)
103, 7, 8, 9syl3anc 1368 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)):π‘ŒβŸΆβˆͺ 𝐾)
11 eqid 2725 . . . . . 6 (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) = (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦))
1211fmpt 7113 . . . . 5 (βˆ€π‘¦ ∈ π‘Œ (π‘₯𝐹𝑦) ∈ βˆͺ 𝐾 ↔ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)):π‘ŒβŸΆβˆͺ 𝐾)
1310, 12sylibr 233 . . . 4 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ βˆ€π‘¦ ∈ π‘Œ (π‘₯𝐹𝑦) ∈ βˆͺ 𝐾)
1413ralrimiva 3136 . . 3 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ π‘Œ (π‘₯𝐹𝑦) ∈ βˆͺ 𝐾)
15 ffnov 7542 . . 3 (𝐹:(𝑋 Γ— π‘Œ)⟢βˆͺ 𝐾 ↔ (𝐹 Fn (𝑋 Γ— π‘Œ) ∧ βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ π‘Œ (π‘₯𝐹𝑦) ∈ βˆͺ 𝐾))
161, 14, 15sylanbrc 581 . 2 (πœ‘ β†’ 𝐹:(𝑋 Γ— π‘Œ)⟢βˆͺ 𝐾)
17 cnvimass 6078 . . . . . . . 8 (◑𝐹 β€œ 𝑒) βŠ† dom 𝐹
181adantr 479 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ 𝐹 Fn (𝑋 Γ— π‘Œ))
1918fndmd 6652 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ dom 𝐹 = (𝑋 Γ— π‘Œ))
2017, 19sseqtrid 4024 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (◑𝐹 β€œ 𝑒) βŠ† (𝑋 Γ— π‘Œ))
21 relxp 5688 . . . . . . 7 Rel (𝑋 Γ— π‘Œ)
22 relss 5775 . . . . . . 7 ((◑𝐹 β€œ 𝑒) βŠ† (𝑋 Γ— π‘Œ) β†’ (Rel (𝑋 Γ— π‘Œ) β†’ Rel (◑𝐹 β€œ 𝑒)))
2320, 21, 22mpisyl 21 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ Rel (◑𝐹 β€œ 𝑒))
24 elpreima 7060 . . . . . . . 8 (𝐹 Fn (𝑋 Γ— π‘Œ) β†’ (⟨π‘₯, π‘§βŸ© ∈ (◑𝐹 β€œ 𝑒) ↔ (⟨π‘₯, π‘§βŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) ∈ 𝑒)))
2518, 24syl 17 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (⟨π‘₯, π‘§βŸ© ∈ (◑𝐹 β€œ 𝑒) ↔ (⟨π‘₯, π‘§βŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) ∈ 𝑒)))
26 opelxp 5706 . . . . . . . . 9 (⟨π‘₯, π‘§βŸ© ∈ (𝑋 Γ— π‘Œ) ↔ (π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ))
27 df-ov 7417 . . . . . . . . . . 11 (π‘₯𝐹𝑧) = (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©)
2827eqcomi 2734 . . . . . . . . . 10 (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) = (π‘₯𝐹𝑧)
2928eleq1i 2816 . . . . . . . . 9 ((πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) ∈ 𝑒 ↔ (π‘₯𝐹𝑧) ∈ 𝑒)
3026, 29anbi12i 626 . . . . . . . 8 ((⟨π‘₯, π‘§βŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) ∈ 𝑒) ↔ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒))
31 simprll 777 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ π‘₯ ∈ 𝑋)
32 snelpwi 5437 . . . . . . . . . . . 12 (π‘₯ ∈ 𝑋 β†’ {π‘₯} ∈ 𝒫 𝑋)
3331, 32syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ {π‘₯} ∈ 𝒫 𝑋)
3411mptpreima 6235 . . . . . . . . . . . 12 (β—‘(𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) β€œ 𝑒) = {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}
358adantrr 715 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ)) β†’ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
3635ad2ant2r 745 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
37 simplr 767 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ 𝑒 ∈ 𝐾)
38 cnima 23185 . . . . . . . . . . . . 13 (((𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) ∈ (𝐽 Cn 𝐾) ∧ 𝑒 ∈ 𝐾) β†’ (β—‘(𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) β€œ 𝑒) ∈ 𝐽)
3936, 37, 38syl2anc 582 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ (β—‘(𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) β€œ 𝑒) ∈ 𝐽)
4034, 39eqeltrrid 2830 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} ∈ 𝐽)
41 simprlr 778 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ 𝑧 ∈ π‘Œ)
42 simprr 771 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ (π‘₯𝐹𝑧) ∈ 𝑒)
43 vsnid 4659 . . . . . . . . . . . . . 14 π‘₯ ∈ {π‘₯}
44 opelxp 5706 . . . . . . . . . . . . . 14 (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ↔ (π‘₯ ∈ {π‘₯} ∧ 𝑧 ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}))
4543, 44mpbiran 707 . . . . . . . . . . . . 13 (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ↔ 𝑧 ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})
46 oveq2 7422 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 β†’ (π‘₯𝐹𝑦) = (π‘₯𝐹𝑧))
4746eleq1d 2810 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 β†’ ((π‘₯𝐹𝑦) ∈ 𝑒 ↔ (π‘₯𝐹𝑧) ∈ 𝑒))
4847elrab 3674 . . . . . . . . . . . . 13 (𝑧 ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} ↔ (𝑧 ∈ π‘Œ ∧ (π‘₯𝐹𝑧) ∈ 𝑒))
4945, 48bitri 274 . . . . . . . . . . . 12 (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ↔ (𝑧 ∈ π‘Œ ∧ (π‘₯𝐹𝑧) ∈ 𝑒))
5041, 42, 49sylanbrc 581 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ ⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}))
51 relxp 5688 . . . . . . . . . . . . 13 Rel ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})
5251a1i 11 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ Rel ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}))
53 opelxp 5706 . . . . . . . . . . . . 13 (βŸ¨π‘›, π‘šβŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ↔ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}))
5431snssd 4806 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ {π‘₯} βŠ† 𝑋)
5554sselda 3972 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ 𝑛 ∈ {π‘₯}) β†’ 𝑛 ∈ 𝑋)
5655adantrr 715 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ 𝑛 ∈ 𝑋)
57 elrabi 3668 . . . . . . . . . . . . . . . . 17 (π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ π‘š ∈ π‘Œ)
5857ad2antll 727 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ π‘š ∈ π‘Œ)
5956, 58opelxpd 5709 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ βŸ¨π‘›, π‘šβŸ© ∈ (𝑋 Γ— π‘Œ))
60 df-ov 7417 . . . . . . . . . . . . . . . . 17 (π‘›πΉπ‘š) = (πΉβ€˜βŸ¨π‘›, π‘šβŸ©)
61 elsni 4639 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ {π‘₯} β†’ 𝑛 = π‘₯)
6261ad2antrl 726 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ 𝑛 = π‘₯)
6362oveq1d 7429 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ (π‘›πΉπ‘š) = (π‘₯πΉπ‘š))
6460, 63eqtr3id 2779 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ (πΉβ€˜βŸ¨π‘›, π‘šβŸ©) = (π‘₯πΉπ‘š))
65 oveq2 7422 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = π‘š β†’ (π‘₯𝐹𝑦) = (π‘₯πΉπ‘š))
6665eleq1d 2810 . . . . . . . . . . . . . . . . . . 19 (𝑦 = π‘š β†’ ((π‘₯𝐹𝑦) ∈ 𝑒 ↔ (π‘₯πΉπ‘š) ∈ 𝑒))
6766elrab 3674 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} ↔ (π‘š ∈ π‘Œ ∧ (π‘₯πΉπ‘š) ∈ 𝑒))
6867simprbi 495 . . . . . . . . . . . . . . . . 17 (π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ (π‘₯πΉπ‘š) ∈ 𝑒)
6968ad2antll 727 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ (π‘₯πΉπ‘š) ∈ 𝑒)
7064, 69eqeltrd 2825 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ (πΉβ€˜βŸ¨π‘›, π‘šβŸ©) ∈ 𝑒)
71 elpreima 7060 . . . . . . . . . . . . . . . . 17 (𝐹 Fn (𝑋 Γ— π‘Œ) β†’ (βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒) ↔ (βŸ¨π‘›, π‘šβŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘›, π‘šβŸ©) ∈ 𝑒)))
721, 71syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒) ↔ (βŸ¨π‘›, π‘šβŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘›, π‘šβŸ©) ∈ 𝑒)))
7372ad3antrrr 728 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ (βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒) ↔ (βŸ¨π‘›, π‘šβŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘›, π‘šβŸ©) ∈ 𝑒)))
7459, 70, 73mpbir2and 711 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒))
7574ex 411 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ ((𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) β†’ βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒)))
7653, 75biimtrid 241 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ (βŸ¨π‘›, π‘šβŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) β†’ βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒)))
7752, 76relssdv 5782 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) βŠ† (◑𝐹 β€œ 𝑒))
78 xpeq1 5684 . . . . . . . . . . . . . 14 (π‘Ž = {π‘₯} β†’ (π‘Ž Γ— 𝑏) = ({π‘₯} Γ— 𝑏))
7978eleq2d 2811 . . . . . . . . . . . . 13 (π‘Ž = {π‘₯} β†’ (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ↔ ⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— 𝑏)))
8078sseq1d 4003 . . . . . . . . . . . . 13 (π‘Ž = {π‘₯} β†’ ((π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒) ↔ ({π‘₯} Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
8179, 80anbi12d 630 . . . . . . . . . . . 12 (π‘Ž = {π‘₯} β†’ ((⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)) ↔ (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— 𝑏) ∧ ({π‘₯} Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))))
82 xpeq2 5691 . . . . . . . . . . . . . 14 (𝑏 = {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ ({π‘₯} Γ— 𝑏) = ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}))
8382eleq2d 2811 . . . . . . . . . . . . 13 (𝑏 = {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— 𝑏) ↔ ⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})))
8482sseq1d 4003 . . . . . . . . . . . . 13 (𝑏 = {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ (({π‘₯} Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒) ↔ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) βŠ† (◑𝐹 β€œ 𝑒)))
8583, 84anbi12d 630 . . . . . . . . . . . 12 (𝑏 = {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ ((⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— 𝑏) ∧ ({π‘₯} Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)) ↔ (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ∧ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) βŠ† (◑𝐹 β€œ 𝑒))))
8681, 85rspc2ev 3614 . . . . . . . . . . 11 (({π‘₯} ∈ 𝒫 𝑋 ∧ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} ∈ 𝐽 ∧ (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ∧ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) βŠ† (◑𝐹 β€œ 𝑒))) β†’ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
8733, 40, 50, 77, 86syl112anc 1371 . . . . . . . . . 10 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
88 opex 5458 . . . . . . . . . . 11 ⟨π‘₯, π‘§βŸ© ∈ V
89 eleq1 2813 . . . . . . . . . . . . 13 (𝑣 = ⟨π‘₯, π‘§βŸ© β†’ (𝑣 ∈ (π‘Ž Γ— 𝑏) ↔ ⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏)))
9089anbi1d 629 . . . . . . . . . . . 12 (𝑣 = ⟨π‘₯, π‘§βŸ© β†’ ((𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)) ↔ (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))))
91902rexbidv 3210 . . . . . . . . . . 11 (𝑣 = ⟨π‘₯, π‘§βŸ© β†’ (βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)) ↔ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))))
9288, 91elab 3659 . . . . . . . . . 10 (⟨π‘₯, π‘§βŸ© ∈ {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))} ↔ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
9387, 92sylibr 233 . . . . . . . . 9 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ ⟨π‘₯, π‘§βŸ© ∈ {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))})
9493ex 411 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒) β†’ ⟨π‘₯, π‘§βŸ© ∈ {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))}))
9530, 94biimtrid 241 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ ((⟨π‘₯, π‘§βŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) ∈ 𝑒) β†’ ⟨π‘₯, π‘§βŸ© ∈ {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))}))
9625, 95sylbid 239 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (⟨π‘₯, π‘§βŸ© ∈ (◑𝐹 β€œ 𝑒) β†’ ⟨π‘₯, π‘§βŸ© ∈ {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))}))
9723, 96relssdv 5782 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (◑𝐹 β€œ 𝑒) βŠ† {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))})
98 ssabral 4049 . . . . 5 ((◑𝐹 β€œ 𝑒) βŠ† {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))} ↔ βˆ€π‘£ ∈ (◑𝐹 β€œ 𝑒)βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
9997, 98sylib 217 . . . 4 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ βˆ€π‘£ ∈ (◑𝐹 β€œ 𝑒)βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
100 txdis1cn.x . . . . . . 7 (πœ‘ β†’ 𝑋 ∈ 𝑉)
101 distopon 22916 . . . . . . 7 (𝑋 ∈ 𝑉 β†’ 𝒫 𝑋 ∈ (TopOnβ€˜π‘‹))
102100, 101syl 17 . . . . . 6 (πœ‘ β†’ 𝒫 𝑋 ∈ (TopOnβ€˜π‘‹))
103102adantr 479 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ 𝒫 𝑋 ∈ (TopOnβ€˜π‘‹))
1042adantr 479 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ 𝐽 ∈ (TopOnβ€˜π‘Œ))
105 eltx 23488 . . . . 5 ((𝒫 𝑋 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ (TopOnβ€˜π‘Œ)) β†’ ((◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽) ↔ βˆ€π‘£ ∈ (◑𝐹 β€œ 𝑒)βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))))
106103, 104, 105syl2anc 582 . . . 4 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ ((◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽) ↔ βˆ€π‘£ ∈ (◑𝐹 β€œ 𝑒)βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))))
10799, 106mpbird 256 . . 3 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽))
108107ralrimiva 3136 . 2 (πœ‘ β†’ βˆ€π‘’ ∈ 𝐾 (◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽))
109 txtopon 23511 . . . 4 ((𝒫 𝑋 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝒫 𝑋 Γ—t 𝐽) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
110102, 2, 109syl2anc 582 . . 3 (πœ‘ β†’ (𝒫 𝑋 Γ—t 𝐽) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
111 iscn 23155 . . 3 (((𝒫 𝑋 Γ—t 𝐽) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)) ∧ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾)) β†’ (𝐹 ∈ ((𝒫 𝑋 Γ—t 𝐽) Cn 𝐾) ↔ (𝐹:(𝑋 Γ— π‘Œ)⟢βˆͺ 𝐾 ∧ βˆ€π‘’ ∈ 𝐾 (◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽))))
112110, 6, 111syl2anc 582 . 2 (πœ‘ β†’ (𝐹 ∈ ((𝒫 𝑋 Γ—t 𝐽) Cn 𝐾) ↔ (𝐹:(𝑋 Γ— π‘Œ)⟢βˆͺ 𝐾 ∧ βˆ€π‘’ ∈ 𝐾 (◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽))))
11316, 108, 112mpbir2and 711 1 (πœ‘ β†’ 𝐹 ∈ ((𝒫 𝑋 Γ—t 𝐽) Cn 𝐾))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533   ∈ wcel 2098  {cab 2702  βˆ€wral 3051  βˆƒwrex 3060  {crab 3419   βŠ† wss 3939  π’« cpw 4596  {csn 4622  βŸ¨cop 4628  βˆͺ cuni 4901   ↦ cmpt 5224   Γ— cxp 5668  β—‘ccnv 5669  dom cdm 5670   β€œ cima 5673  Rel wrel 5675   Fn wfn 6536  βŸΆwf 6537  β€˜cfv 6541  (class class class)co 7414  Topctop 22811  TopOnctopon 22828   Cn ccn 23144   Γ—t ctx 23480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5292  ax-nul 5299  ax-pow 5357  ax-pr 5421  ax-un 7736
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3465  df-sbc 3769  df-csb 3885  df-dif 3942  df-un 3944  df-in 3946  df-ss 3956  df-nul 4317  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-iun 4991  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5568  df-xp 5676  df-rel 5677  df-cnv 5678  df-co 5679  df-dm 5680  df-rn 5681  df-res 5682  df-ima 5683  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-fv 6549  df-ov 7417  df-oprab 7418  df-mpo 7419  df-1st 7989  df-2nd 7990  df-map 8843  df-topgen 17422  df-top 22812  df-topon 22829  df-bases 22865  df-cn 23147  df-tx 23482
This theorem is referenced by:  tgpmulg2  24014
  Copyright terms: Public domain W3C validator