MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  txdis1cn Structured version   Visualization version   GIF version
Theorem txdis1cn 23494
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 480 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ 𝐽 ∈ (TopOnβ€˜π‘Œ))
4 txdis1cn.k . . . . . . . 8 (πœ‘ β†’ 𝐾 ∈ Top)
5 toptopon2 22775 . . . . . . . 8 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾))
64, 5sylib 217 . . . . . . 7 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾))
76adantr 480 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾))
8 txdis1cn.1 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
9 cnf2 23108 . . . . . 6 ((𝐽 ∈ (TopOnβ€˜π‘Œ) ∧ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾) ∧ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) ∈ (𝐽 Cn 𝐾)) β†’ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)):π‘ŒβŸΆβˆͺ 𝐾)
103, 7, 8, 9syl3anc 1368 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)):π‘ŒβŸΆβˆͺ 𝐾)
11 eqid 2726 . . . . . 6 (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) = (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦))
1211fmpt 7105 . . . . 5 (βˆ€π‘¦ ∈ π‘Œ (π‘₯𝐹𝑦) ∈ βˆͺ 𝐾 ↔ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)):π‘ŒβŸΆβˆͺ 𝐾)
1310, 12sylibr 233 . . . 4 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ βˆ€π‘¦ ∈ π‘Œ (π‘₯𝐹𝑦) ∈ βˆͺ 𝐾)
1413ralrimiva 3140 . . 3 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ π‘Œ (π‘₯𝐹𝑦) ∈ βˆͺ 𝐾)
15 ffnov 7531 . . 3 (𝐹:(𝑋 Γ— π‘Œ)⟢βˆͺ 𝐾 ↔ (𝐹 Fn (𝑋 Γ— π‘Œ) ∧ βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ π‘Œ (π‘₯𝐹𝑦) ∈ βˆͺ 𝐾))
161, 14, 15sylanbrc 582 . 2 (πœ‘ β†’ 𝐹:(𝑋 Γ— π‘Œ)⟢βˆͺ 𝐾)
17 cnvimass 6074 . . . . . . . 8 (◑𝐹 β€œ 𝑒) βŠ† dom 𝐹
181adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ 𝐹 Fn (𝑋 Γ— π‘Œ))
1918fndmd 6648 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ dom 𝐹 = (𝑋 Γ— π‘Œ))
2017, 19sseqtrid 4029 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (◑𝐹 β€œ 𝑒) βŠ† (𝑋 Γ— π‘Œ))
21 relxp 5687 . . . . . . 7 Rel (𝑋 Γ— π‘Œ)
22 relss 5774 . . . . . . 7 ((◑𝐹 β€œ 𝑒) βŠ† (𝑋 Γ— π‘Œ) β†’ (Rel (𝑋 Γ— π‘Œ) β†’ Rel (◑𝐹 β€œ 𝑒)))
2320, 21, 22mpisyl 21 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ Rel (◑𝐹 β€œ 𝑒))
24 elpreima 7053 . . . . . . . 8 (𝐹 Fn (𝑋 Γ— π‘Œ) β†’ (⟨π‘₯, π‘§βŸ© ∈ (◑𝐹 β€œ 𝑒) ↔ (⟨π‘₯, π‘§βŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) ∈ 𝑒)))
2518, 24syl 17 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (⟨π‘₯, π‘§βŸ© ∈ (◑𝐹 β€œ 𝑒) ↔ (⟨π‘₯, π‘§βŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) ∈ 𝑒)))
26 opelxp 5705 . . . . . . . . 9 (⟨π‘₯, π‘§βŸ© ∈ (𝑋 Γ— π‘Œ) ↔ (π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ))
27 df-ov 7408 . . . . . . . . . . 11 (π‘₯𝐹𝑧) = (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©)
2827eqcomi 2735 . . . . . . . . . 10 (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) = (π‘₯𝐹𝑧)
2928eleq1i 2818 . . . . . . . . 9 ((πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) ∈ 𝑒 ↔ (π‘₯𝐹𝑧) ∈ 𝑒)
3026, 29anbi12i 626 . . . . . . . 8 ((⟨π‘₯, π‘§βŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) ∈ 𝑒) ↔ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒))
31 simprll 776 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ π‘₯ ∈ 𝑋)
32 snelpwi 5436 . . . . . . . . . . . 12 (π‘₯ ∈ 𝑋 β†’ {π‘₯} ∈ 𝒫 𝑋)
3331, 32syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ {π‘₯} ∈ 𝒫 𝑋)
3411mptpreima 6231 . . . . . . . . . . . 12 (β—‘(𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) β€œ 𝑒) = {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}
358adantrr 714 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ)) β†’ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
3635ad2ant2r 744 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
37 simplr 766 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ 𝑒 ∈ 𝐾)
38 cnima 23124 . . . . . . . . . . . . 13 (((𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) ∈ (𝐽 Cn 𝐾) ∧ 𝑒 ∈ 𝐾) β†’ (β—‘(𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) β€œ 𝑒) ∈ 𝐽)
3936, 37, 38syl2anc 583 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ (β—‘(𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) β€œ 𝑒) ∈ 𝐽)
4034, 39eqeltrrid 2832 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} ∈ 𝐽)
41 simprlr 777 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ 𝑧 ∈ π‘Œ)
42 simprr 770 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ (π‘₯𝐹𝑧) ∈ 𝑒)
43 vsnid 4660 . . . . . . . . . . . . . 14 π‘₯ ∈ {π‘₯}
44 opelxp 5705 . . . . . . . . . . . . . 14 (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ↔ (π‘₯ ∈ {π‘₯} ∧ 𝑧 ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}))
4543, 44mpbiran 706 . . . . . . . . . . . . 13 (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ↔ 𝑧 ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})
46 oveq2 7413 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 β†’ (π‘₯𝐹𝑦) = (π‘₯𝐹𝑧))
4746eleq1d 2812 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 β†’ ((π‘₯𝐹𝑦) ∈ 𝑒 ↔ (π‘₯𝐹𝑧) ∈ 𝑒))
4847elrab 3678 . . . . . . . . . . . . 13 (𝑧 ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} ↔ (𝑧 ∈ π‘Œ ∧ (π‘₯𝐹𝑧) ∈ 𝑒))
4945, 48bitri 275 . . . . . . . . . . . 12 (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ↔ (𝑧 ∈ π‘Œ ∧ (π‘₯𝐹𝑧) ∈ 𝑒))
5041, 42, 49sylanbrc 582 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ ⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}))
51 relxp 5687 . . . . . . . . . . . . 13 Rel ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})
5251a1i 11 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ Rel ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}))
53 opelxp 5705 . . . . . . . . . . . . 13 (βŸ¨π‘›, π‘šβŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ↔ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}))
5431snssd 4807 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ {π‘₯} βŠ† 𝑋)
5554sselda 3977 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ 𝑛 ∈ {π‘₯}) β†’ 𝑛 ∈ 𝑋)
5655adantrr 714 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ 𝑛 ∈ 𝑋)
57 elrabi 3672 . . . . . . . . . . . . . . . . 17 (π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ π‘š ∈ π‘Œ)
5857ad2antll 726 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ π‘š ∈ π‘Œ)
5956, 58opelxpd 5708 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ βŸ¨π‘›, π‘šβŸ© ∈ (𝑋 Γ— π‘Œ))
60 df-ov 7408 . . . . . . . . . . . . . . . . 17 (π‘›πΉπ‘š) = (πΉβ€˜βŸ¨π‘›, π‘šβŸ©)
61 elsni 4640 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ {π‘₯} β†’ 𝑛 = π‘₯)
6261ad2antrl 725 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ 𝑛 = π‘₯)
6362oveq1d 7420 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ (π‘›πΉπ‘š) = (π‘₯πΉπ‘š))
6460, 63eqtr3id 2780 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ (πΉβ€˜βŸ¨π‘›, π‘šβŸ©) = (π‘₯πΉπ‘š))
65 oveq2 7413 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = π‘š β†’ (π‘₯𝐹𝑦) = (π‘₯πΉπ‘š))
6665eleq1d 2812 . . . . . . . . . . . . . . . . . . 19 (𝑦 = π‘š β†’ ((π‘₯𝐹𝑦) ∈ 𝑒 ↔ (π‘₯πΉπ‘š) ∈ 𝑒))
6766elrab 3678 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} ↔ (π‘š ∈ π‘Œ ∧ (π‘₯πΉπ‘š) ∈ 𝑒))
6867simprbi 496 . . . . . . . . . . . . . . . . 17 (π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ (π‘₯πΉπ‘š) ∈ 𝑒)
6968ad2antll 726 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ (π‘₯πΉπ‘š) ∈ 𝑒)
7064, 69eqeltrd 2827 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ (πΉβ€˜βŸ¨π‘›, π‘šβŸ©) ∈ 𝑒)
71 elpreima 7053 . . . . . . . . . . . . . . . . 17 (𝐹 Fn (𝑋 Γ— π‘Œ) β†’ (βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒) ↔ (βŸ¨π‘›, π‘šβŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘›, π‘šβŸ©) ∈ 𝑒)))
721, 71syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒) ↔ (βŸ¨π‘›, π‘šβŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘›, π‘šβŸ©) ∈ 𝑒)))
7372ad3antrrr 727 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ (βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒) ↔ (βŸ¨π‘›, π‘šβŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘›, π‘šβŸ©) ∈ 𝑒)))
7459, 70, 73mpbir2and 710 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒))
7574ex 412 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ ((𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) β†’ βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒)))
7653, 75biimtrid 241 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ (βŸ¨π‘›, π‘šβŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) β†’ βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒)))
7752, 76relssdv 5781 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) βŠ† (◑𝐹 β€œ 𝑒))
78 xpeq1 5683 . . . . . . . . . . . . . 14 (π‘Ž = {π‘₯} β†’ (π‘Ž Γ— 𝑏) = ({π‘₯} Γ— 𝑏))
7978eleq2d 2813 . . . . . . . . . . . . 13 (π‘Ž = {π‘₯} β†’ (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ↔ ⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— 𝑏)))
8078sseq1d 4008 . . . . . . . . . . . . 13 (π‘Ž = {π‘₯} β†’ ((π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒) ↔ ({π‘₯} Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
8179, 80anbi12d 630 . . . . . . . . . . . 12 (π‘Ž = {π‘₯} β†’ ((⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)) ↔ (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— 𝑏) ∧ ({π‘₯} Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))))
82 xpeq2 5690 . . . . . . . . . . . . . 14 (𝑏 = {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ ({π‘₯} Γ— 𝑏) = ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}))
8382eleq2d 2813 . . . . . . . . . . . . 13 (𝑏 = {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— 𝑏) ↔ ⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})))
8482sseq1d 4008 . . . . . . . . . . . . 13 (𝑏 = {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ (({π‘₯} Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒) ↔ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) βŠ† (◑𝐹 β€œ 𝑒)))
8583, 84anbi12d 630 . . . . . . . . . . . 12 (𝑏 = {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ ((⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— 𝑏) ∧ ({π‘₯} Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)) ↔ (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ∧ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) βŠ† (◑𝐹 β€œ 𝑒))))
8681, 85rspc2ev 3619 . . . . . . . . . . 11 (({π‘₯} ∈ 𝒫 𝑋 ∧ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} ∈ 𝐽 ∧ (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ∧ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) βŠ† (◑𝐹 β€œ 𝑒))) β†’ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
8733, 40, 50, 77, 86syl112anc 1371 . . . . . . . . . 10 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
88 opex 5457 . . . . . . . . . . 11 ⟨π‘₯, π‘§βŸ© ∈ V
89 eleq1 2815 . . . . . . . . . . . . 13 (𝑣 = ⟨π‘₯, π‘§βŸ© β†’ (𝑣 ∈ (π‘Ž Γ— 𝑏) ↔ ⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏)))
9089anbi1d 629 . . . . . . . . . . . 12 (𝑣 = ⟨π‘₯, π‘§βŸ© β†’ ((𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)) ↔ (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))))
91902rexbidv 3213 . . . . . . . . . . 11 (𝑣 = ⟨π‘₯, π‘§βŸ© β†’ (βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)) ↔ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))))
9288, 91elab 3663 . . . . . . . . . 10 (⟨π‘₯, π‘§βŸ© ∈ {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))} ↔ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
9387, 92sylibr 233 . . . . . . . . 9 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ ⟨π‘₯, π‘§βŸ© ∈ {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))})
9493ex 412 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒) β†’ ⟨π‘₯, π‘§βŸ© ∈ {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))}))
9530, 94biimtrid 241 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ ((⟨π‘₯, π‘§βŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) ∈ 𝑒) β†’ ⟨π‘₯, π‘§βŸ© ∈ {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))}))
9625, 95sylbid 239 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (⟨π‘₯, π‘§βŸ© ∈ (◑𝐹 β€œ 𝑒) β†’ ⟨π‘₯, π‘§βŸ© ∈ {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))}))
9723, 96relssdv 5781 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (◑𝐹 β€œ 𝑒) βŠ† {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))})
98 ssabral 4054 . . . . 5 ((◑𝐹 β€œ 𝑒) βŠ† {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))} ↔ βˆ€π‘£ ∈ (◑𝐹 β€œ 𝑒)βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
9997, 98sylib 217 . . . 4 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ βˆ€π‘£ ∈ (◑𝐹 β€œ 𝑒)βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
100 txdis1cn.x . . . . . . 7 (πœ‘ β†’ 𝑋 ∈ 𝑉)
101 distopon 22855 . . . . . . 7 (𝑋 ∈ 𝑉 β†’ 𝒫 𝑋 ∈ (TopOnβ€˜π‘‹))
102100, 101syl 17 . . . . . 6 (πœ‘ β†’ 𝒫 𝑋 ∈ (TopOnβ€˜π‘‹))
103102adantr 480 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ 𝒫 𝑋 ∈ (TopOnβ€˜π‘‹))
1042adantr 480 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ 𝐽 ∈ (TopOnβ€˜π‘Œ))
105 eltx 23427 . . . . 5 ((𝒫 𝑋 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ (TopOnβ€˜π‘Œ)) β†’ ((◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽) ↔ βˆ€π‘£ ∈ (◑𝐹 β€œ 𝑒)βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))))
106103, 104, 105syl2anc 583 . . . 4 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ ((◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽) ↔ βˆ€π‘£ ∈ (◑𝐹 β€œ 𝑒)βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))))
10799, 106mpbird 257 . . 3 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽))
108107ralrimiva 3140 . 2 (πœ‘ β†’ βˆ€π‘’ ∈ 𝐾 (◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽))
109 txtopon 23450 . . . 4 ((𝒫 𝑋 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝒫 𝑋 Γ—t 𝐽) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
110102, 2, 109syl2anc 583 . . 3 (πœ‘ β†’ (𝒫 𝑋 Γ—t 𝐽) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
111 iscn 23094 . . 3 (((𝒫 𝑋 Γ—t 𝐽) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)) ∧ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾)) β†’ (𝐹 ∈ ((𝒫 𝑋 Γ—t 𝐽) Cn 𝐾) ↔ (𝐹:(𝑋 Γ— π‘Œ)⟢βˆͺ 𝐾 ∧ βˆ€π‘’ ∈ 𝐾 (◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽))))
112110, 6, 111syl2anc 583 . 2 (πœ‘ β†’ (𝐹 ∈ ((𝒫 𝑋 Γ—t 𝐽) Cn 𝐾) ↔ (𝐹:(𝑋 Γ— π‘Œ)⟢βˆͺ 𝐾 ∧ βˆ€π‘’ ∈ 𝐾 (◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽))))
11316, 108, 112mpbir2and 710 1 (πœ‘ β†’ 𝐹 ∈ ((𝒫 𝑋 Γ—t 𝐽) Cn 𝐾))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533   ∈ wcel 2098  {cab 2703  βˆ€wral 3055  βˆƒwrex 3064  {crab 3426   βŠ† wss 3943  π’« cpw 4597  {csn 4623  βŸ¨cop 4629  βˆͺ cuni 4902   ↦ cmpt 5224   Γ— cxp 5667  β—‘ccnv 5668  dom cdm 5669   β€œ cima 5672  Rel wrel 5674   Fn wfn 6532  βŸΆwf 6533  β€˜cfv 6537  (class class class)co 7405  Topctop 22750  TopOnctopon 22767   Cn ccn 23083   Γ—t ctx 23419
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 2163  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  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 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7408  df-oprab 7409  df-mpo 7410  df-1st 7974  df-2nd 7975  df-map 8824  df-topgen 17398  df-top 22751  df-topon 22768  df-bases 22804  df-cn 23086  df-tx 23421
This theorem is referenced by:  tgpmulg2  23953
  Copyright terms: Public domain W3C validator