MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  txdis1cn Structured version   Visualization version   GIF version
Theorem txdis1cn 23130
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 481 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ 𝐽 ∈ (TopOnβ€˜π‘Œ))
4 txdis1cn.k . . . . . . . 8 (πœ‘ β†’ 𝐾 ∈ Top)
5 toptopon2 22411 . . . . . . . 8 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾))
64, 5sylib 217 . . . . . . 7 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾))
76adantr 481 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾))
8 txdis1cn.1 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
9 cnf2 22744 . . . . . 6 ((𝐽 ∈ (TopOnβ€˜π‘Œ) ∧ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾) ∧ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) ∈ (𝐽 Cn 𝐾)) β†’ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)):π‘ŒβŸΆβˆͺ 𝐾)
103, 7, 8, 9syl3anc 1371 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)):π‘ŒβŸΆβˆͺ 𝐾)
11 eqid 2732 . . . . . 6 (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) = (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦))
1211fmpt 7106 . . . . 5 (βˆ€π‘¦ ∈ π‘Œ (π‘₯𝐹𝑦) ∈ βˆͺ 𝐾 ↔ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)):π‘ŒβŸΆβˆͺ 𝐾)
1310, 12sylibr 233 . . . 4 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ βˆ€π‘¦ ∈ π‘Œ (π‘₯𝐹𝑦) ∈ βˆͺ 𝐾)
1413ralrimiva 3146 . . 3 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ π‘Œ (π‘₯𝐹𝑦) ∈ βˆͺ 𝐾)
15 ffnov 7531 . . 3 (𝐹:(𝑋 Γ— π‘Œ)⟢βˆͺ 𝐾 ↔ (𝐹 Fn (𝑋 Γ— π‘Œ) ∧ βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ π‘Œ (π‘₯𝐹𝑦) ∈ βˆͺ 𝐾))
161, 14, 15sylanbrc 583 . 2 (πœ‘ β†’ 𝐹:(𝑋 Γ— π‘Œ)⟢βˆͺ 𝐾)
17 cnvimass 6077 . . . . . . . 8 (◑𝐹 β€œ 𝑒) βŠ† dom 𝐹
181adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ 𝐹 Fn (𝑋 Γ— π‘Œ))
1918fndmd 6651 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ dom 𝐹 = (𝑋 Γ— π‘Œ))
2017, 19sseqtrid 4033 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (◑𝐹 β€œ 𝑒) βŠ† (𝑋 Γ— π‘Œ))
21 relxp 5693 . . . . . . 7 Rel (𝑋 Γ— π‘Œ)
22 relss 5779 . . . . . . 7 ((◑𝐹 β€œ 𝑒) βŠ† (𝑋 Γ— π‘Œ) β†’ (Rel (𝑋 Γ— π‘Œ) β†’ Rel (◑𝐹 β€œ 𝑒)))
2320, 21, 22mpisyl 21 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ Rel (◑𝐹 β€œ 𝑒))
24 elpreima 7056 . . . . . . . 8 (𝐹 Fn (𝑋 Γ— π‘Œ) β†’ (⟨π‘₯, π‘§βŸ© ∈ (◑𝐹 β€œ 𝑒) ↔ (⟨π‘₯, π‘§βŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) ∈ 𝑒)))
2518, 24syl 17 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (⟨π‘₯, π‘§βŸ© ∈ (◑𝐹 β€œ 𝑒) ↔ (⟨π‘₯, π‘§βŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) ∈ 𝑒)))
26 opelxp 5711 . . . . . . . . 9 (⟨π‘₯, π‘§βŸ© ∈ (𝑋 Γ— π‘Œ) ↔ (π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ))
27 df-ov 7408 . . . . . . . . . . 11 (π‘₯𝐹𝑧) = (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©)
2827eqcomi 2741 . . . . . . . . . 10 (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) = (π‘₯𝐹𝑧)
2928eleq1i 2824 . . . . . . . . 9 ((πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) ∈ 𝑒 ↔ (π‘₯𝐹𝑧) ∈ 𝑒)
3026, 29anbi12i 627 . . . . . . . 8 ((⟨π‘₯, π‘§βŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) ∈ 𝑒) ↔ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒))
31 simprll 777 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ π‘₯ ∈ 𝑋)
32 snelpwi 5442 . . . . . . . . . . . 12 (π‘₯ ∈ 𝑋 β†’ {π‘₯} ∈ 𝒫 𝑋)
3331, 32syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ {π‘₯} ∈ 𝒫 𝑋)
3411mptpreima 6234 . . . . . . . . . . . 12 (β—‘(𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) β€œ 𝑒) = {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}
358adantrr 715 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ)) β†’ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
3635ad2ant2r 745 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
37 simplr 767 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ 𝑒 ∈ 𝐾)
38 cnima 22760 . . . . . . . . . . . . 13 (((𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) ∈ (𝐽 Cn 𝐾) ∧ 𝑒 ∈ 𝐾) β†’ (β—‘(𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) β€œ 𝑒) ∈ 𝐽)
3936, 37, 38syl2anc 584 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ (β—‘(𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) β€œ 𝑒) ∈ 𝐽)
4034, 39eqeltrrid 2838 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} ∈ 𝐽)
41 simprlr 778 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ 𝑧 ∈ π‘Œ)
42 simprr 771 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ (π‘₯𝐹𝑧) ∈ 𝑒)
43 vsnid 4664 . . . . . . . . . . . . . 14 π‘₯ ∈ {π‘₯}
44 opelxp 5711 . . . . . . . . . . . . . 14 (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ↔ (π‘₯ ∈ {π‘₯} ∧ 𝑧 ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}))
4543, 44mpbiran 707 . . . . . . . . . . . . 13 (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ↔ 𝑧 ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})
46 oveq2 7413 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 β†’ (π‘₯𝐹𝑦) = (π‘₯𝐹𝑧))
4746eleq1d 2818 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 β†’ ((π‘₯𝐹𝑦) ∈ 𝑒 ↔ (π‘₯𝐹𝑧) ∈ 𝑒))
4847elrab 3682 . . . . . . . . . . . . 13 (𝑧 ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} ↔ (𝑧 ∈ π‘Œ ∧ (π‘₯𝐹𝑧) ∈ 𝑒))
4945, 48bitri 274 . . . . . . . . . . . 12 (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ↔ (𝑧 ∈ π‘Œ ∧ (π‘₯𝐹𝑧) ∈ 𝑒))
5041, 42, 49sylanbrc 583 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ ⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}))
51 relxp 5693 . . . . . . . . . . . . 13 Rel ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})
5251a1i 11 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ Rel ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}))
53 opelxp 5711 . . . . . . . . . . . . 13 (βŸ¨π‘›, π‘šβŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ↔ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}))
5431snssd 4811 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ {π‘₯} βŠ† 𝑋)
5554sselda 3981 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ 𝑛 ∈ {π‘₯}) β†’ 𝑛 ∈ 𝑋)
5655adantrr 715 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ 𝑛 ∈ 𝑋)
57 elrabi 3676 . . . . . . . . . . . . . . . . 17 (π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ π‘š ∈ π‘Œ)
5857ad2antll 727 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ π‘š ∈ π‘Œ)
5956, 58opelxpd 5713 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ βŸ¨π‘›, π‘šβŸ© ∈ (𝑋 Γ— π‘Œ))
60 df-ov 7408 . . . . . . . . . . . . . . . . 17 (π‘›πΉπ‘š) = (πΉβ€˜βŸ¨π‘›, π‘šβŸ©)
61 elsni 4644 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ {π‘₯} β†’ 𝑛 = π‘₯)
6261ad2antrl 726 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ 𝑛 = π‘₯)
6362oveq1d 7420 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ (π‘›πΉπ‘š) = (π‘₯πΉπ‘š))
6460, 63eqtr3id 2786 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ (πΉβ€˜βŸ¨π‘›, π‘šβŸ©) = (π‘₯πΉπ‘š))
65 oveq2 7413 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = π‘š β†’ (π‘₯𝐹𝑦) = (π‘₯πΉπ‘š))
6665eleq1d 2818 . . . . . . . . . . . . . . . . . . 19 (𝑦 = π‘š β†’ ((π‘₯𝐹𝑦) ∈ 𝑒 ↔ (π‘₯πΉπ‘š) ∈ 𝑒))
6766elrab 3682 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} ↔ (π‘š ∈ π‘Œ ∧ (π‘₯πΉπ‘š) ∈ 𝑒))
6867simprbi 497 . . . . . . . . . . . . . . . . 17 (π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ (π‘₯πΉπ‘š) ∈ 𝑒)
6968ad2antll 727 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ (π‘₯πΉπ‘š) ∈ 𝑒)
7064, 69eqeltrd 2833 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ (πΉβ€˜βŸ¨π‘›, π‘šβŸ©) ∈ 𝑒)
71 elpreima 7056 . . . . . . . . . . . . . . . . 17 (𝐹 Fn (𝑋 Γ— π‘Œ) β†’ (βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒) ↔ (βŸ¨π‘›, π‘šβŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘›, π‘šβŸ©) ∈ 𝑒)))
721, 71syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒) ↔ (βŸ¨π‘›, π‘šβŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘›, π‘šβŸ©) ∈ 𝑒)))
7372ad3antrrr 728 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ (βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒) ↔ (βŸ¨π‘›, π‘šβŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘›, π‘šβŸ©) ∈ 𝑒)))
7459, 70, 73mpbir2and 711 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒))
7574ex 413 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ ((𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) β†’ βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒)))
7653, 75biimtrid 241 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ (βŸ¨π‘›, π‘šβŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) β†’ βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒)))
7752, 76relssdv 5786 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) βŠ† (◑𝐹 β€œ 𝑒))
78 xpeq1 5689 . . . . . . . . . . . . . 14 (π‘Ž = {π‘₯} β†’ (π‘Ž Γ— 𝑏) = ({π‘₯} Γ— 𝑏))
7978eleq2d 2819 . . . . . . . . . . . . 13 (π‘Ž = {π‘₯} β†’ (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ↔ ⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— 𝑏)))
8078sseq1d 4012 . . . . . . . . . . . . 13 (π‘Ž = {π‘₯} β†’ ((π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒) ↔ ({π‘₯} Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
8179, 80anbi12d 631 . . . . . . . . . . . 12 (π‘Ž = {π‘₯} β†’ ((⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)) ↔ (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— 𝑏) ∧ ({π‘₯} Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))))
82 xpeq2 5696 . . . . . . . . . . . . . 14 (𝑏 = {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ ({π‘₯} Γ— 𝑏) = ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}))
8382eleq2d 2819 . . . . . . . . . . . . 13 (𝑏 = {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— 𝑏) ↔ ⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})))
8482sseq1d 4012 . . . . . . . . . . . . 13 (𝑏 = {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ (({π‘₯} Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒) ↔ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) βŠ† (◑𝐹 β€œ 𝑒)))
8583, 84anbi12d 631 . . . . . . . . . . . 12 (𝑏 = {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ ((⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— 𝑏) ∧ ({π‘₯} Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)) ↔ (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ∧ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) βŠ† (◑𝐹 β€œ 𝑒))))
8681, 85rspc2ev 3623 . . . . . . . . . . 11 (({π‘₯} ∈ 𝒫 𝑋 ∧ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} ∈ 𝐽 ∧ (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ∧ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) βŠ† (◑𝐹 β€œ 𝑒))) β†’ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
8733, 40, 50, 77, 86syl112anc 1374 . . . . . . . . . 10 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
88 opex 5463 . . . . . . . . . . 11 ⟨π‘₯, π‘§βŸ© ∈ V
89 eleq1 2821 . . . . . . . . . . . . 13 (𝑣 = ⟨π‘₯, π‘§βŸ© β†’ (𝑣 ∈ (π‘Ž Γ— 𝑏) ↔ ⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏)))
9089anbi1d 630 . . . . . . . . . . . 12 (𝑣 = ⟨π‘₯, π‘§βŸ© β†’ ((𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)) ↔ (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))))
91902rexbidv 3219 . . . . . . . . . . 11 (𝑣 = ⟨π‘₯, π‘§βŸ© β†’ (βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)) ↔ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))))
9288, 91elab 3667 . . . . . . . . . 10 (⟨π‘₯, π‘§βŸ© ∈ {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))} ↔ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
9387, 92sylibr 233 . . . . . . . . 9 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ ⟨π‘₯, π‘§βŸ© ∈ {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))})
9493ex 413 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒) β†’ ⟨π‘₯, π‘§βŸ© ∈ {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))}))
9530, 94biimtrid 241 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ ((⟨π‘₯, π‘§βŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) ∈ 𝑒) β†’ ⟨π‘₯, π‘§βŸ© ∈ {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))}))
9625, 95sylbid 239 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (⟨π‘₯, π‘§βŸ© ∈ (◑𝐹 β€œ 𝑒) β†’ ⟨π‘₯, π‘§βŸ© ∈ {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))}))
9723, 96relssdv 5786 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (◑𝐹 β€œ 𝑒) βŠ† {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))})
98 ssabral 4058 . . . . 5 ((◑𝐹 β€œ 𝑒) βŠ† {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))} ↔ βˆ€π‘£ ∈ (◑𝐹 β€œ 𝑒)βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
9997, 98sylib 217 . . . 4 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ βˆ€π‘£ ∈ (◑𝐹 β€œ 𝑒)βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
100 txdis1cn.x . . . . . . 7 (πœ‘ β†’ 𝑋 ∈ 𝑉)
101 distopon 22491 . . . . . . 7 (𝑋 ∈ 𝑉 β†’ 𝒫 𝑋 ∈ (TopOnβ€˜π‘‹))
102100, 101syl 17 . . . . . 6 (πœ‘ β†’ 𝒫 𝑋 ∈ (TopOnβ€˜π‘‹))
103102adantr 481 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ 𝒫 𝑋 ∈ (TopOnβ€˜π‘‹))
1042adantr 481 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ 𝐽 ∈ (TopOnβ€˜π‘Œ))
105 eltx 23063 . . . . 5 ((𝒫 𝑋 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ (TopOnβ€˜π‘Œ)) β†’ ((◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽) ↔ βˆ€π‘£ ∈ (◑𝐹 β€œ 𝑒)βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))))
106103, 104, 105syl2anc 584 . . . 4 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ ((◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽) ↔ βˆ€π‘£ ∈ (◑𝐹 β€œ 𝑒)βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))))
10799, 106mpbird 256 . . 3 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽))
108107ralrimiva 3146 . 2 (πœ‘ β†’ βˆ€π‘’ ∈ 𝐾 (◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽))
109 txtopon 23086 . . . 4 ((𝒫 𝑋 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝒫 𝑋 Γ—t 𝐽) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
110102, 2, 109syl2anc 584 . . 3 (πœ‘ β†’ (𝒫 𝑋 Γ—t 𝐽) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
111 iscn 22730 . . 3 (((𝒫 𝑋 Γ—t 𝐽) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)) ∧ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾)) β†’ (𝐹 ∈ ((𝒫 𝑋 Γ—t 𝐽) Cn 𝐾) ↔ (𝐹:(𝑋 Γ— π‘Œ)⟢βˆͺ 𝐾 ∧ βˆ€π‘’ ∈ 𝐾 (◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽))))
112110, 6, 111syl2anc 584 . 2 (πœ‘ β†’ (𝐹 ∈ ((𝒫 𝑋 Γ—t 𝐽) Cn 𝐾) ↔ (𝐹:(𝑋 Γ— π‘Œ)⟢βˆͺ 𝐾 ∧ βˆ€π‘’ ∈ 𝐾 (◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽))))
11316, 108, 112mpbir2and 711 1 (πœ‘ β†’ 𝐹 ∈ ((𝒫 𝑋 Γ—t 𝐽) Cn 𝐾))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {cab 2709  βˆ€wral 3061  βˆƒwrex 3070  {crab 3432   βŠ† wss 3947  π’« cpw 4601  {csn 4627  βŸ¨cop 4633  βˆͺ cuni 4907   ↦ cmpt 5230   Γ— cxp 5673  β—‘ccnv 5674  dom cdm 5675   β€œ cima 5678  Rel wrel 5680   Fn wfn 6535  βŸΆwf 6536  β€˜cfv 6540  (class class class)co 7405  Topctop 22386  TopOnctopon 22403   Cn ccn 22719   Γ—t ctx 23055
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-1st 7971  df-2nd 7972  df-map 8818  df-topgen 17385  df-top 22387  df-topon 22404  df-bases 22440  df-cn 22722  df-tx 23057
This theorem is referenced by:  tgpmulg2  23589
  Copyright terms: Public domain W3C validator