ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  txdis1cn GIF version

Theorem txdis1cn 13817
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 276 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ 𝐽 ∈ (TopOnβ€˜π‘Œ))
4 txdis1cn.k . . . . . . . 8 (πœ‘ β†’ 𝐾 ∈ Top)
5 toptopon2 13558 . . . . . . . 8 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾))
64, 5sylib 122 . . . . . . 7 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾))
76adantr 276 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾))
8 txdis1cn.1 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
9 cnf2 13744 . . . . . 6 ((𝐽 ∈ (TopOnβ€˜π‘Œ) ∧ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾) ∧ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) ∈ (𝐽 Cn 𝐾)) β†’ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)):π‘ŒβŸΆβˆͺ 𝐾)
103, 7, 8, 9syl3anc 1238 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)):π‘ŒβŸΆβˆͺ 𝐾)
11 eqid 2177 . . . . . 6 (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) = (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦))
1211fmpt 5668 . . . . 5 (βˆ€π‘¦ ∈ π‘Œ (π‘₯𝐹𝑦) ∈ βˆͺ 𝐾 ↔ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)):π‘ŒβŸΆβˆͺ 𝐾)
1310, 12sylibr 134 . . . 4 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ βˆ€π‘¦ ∈ π‘Œ (π‘₯𝐹𝑦) ∈ βˆͺ 𝐾)
1413ralrimiva 2550 . . 3 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ π‘Œ (π‘₯𝐹𝑦) ∈ βˆͺ 𝐾)
15 ffnov 5981 . . 3 (𝐹:(𝑋 Γ— π‘Œ)⟢βˆͺ 𝐾 ↔ (𝐹 Fn (𝑋 Γ— π‘Œ) ∧ βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ π‘Œ (π‘₯𝐹𝑦) ∈ βˆͺ 𝐾))
161, 14, 15sylanbrc 417 . 2 (πœ‘ β†’ 𝐹:(𝑋 Γ— π‘Œ)⟢βˆͺ 𝐾)
17 cnvimass 4993 . . . . . . . 8 (◑𝐹 β€œ 𝑒) βŠ† dom 𝐹
181adantr 276 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ 𝐹 Fn (𝑋 Γ— π‘Œ))
19 fndm 5317 . . . . . . . . 9 (𝐹 Fn (𝑋 Γ— π‘Œ) β†’ dom 𝐹 = (𝑋 Γ— π‘Œ))
2018, 19syl 14 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ dom 𝐹 = (𝑋 Γ— π‘Œ))
2117, 20sseqtrid 3207 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (◑𝐹 β€œ 𝑒) βŠ† (𝑋 Γ— π‘Œ))
22 relxp 4737 . . . . . . 7 Rel (𝑋 Γ— π‘Œ)
23 relss 4715 . . . . . . 7 ((◑𝐹 β€œ 𝑒) βŠ† (𝑋 Γ— π‘Œ) β†’ (Rel (𝑋 Γ— π‘Œ) β†’ Rel (◑𝐹 β€œ 𝑒)))
2421, 22, 23mpisyl 1446 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ Rel (◑𝐹 β€œ 𝑒))
25 elpreima 5637 . . . . . . . 8 (𝐹 Fn (𝑋 Γ— π‘Œ) β†’ (⟨π‘₯, π‘§βŸ© ∈ (◑𝐹 β€œ 𝑒) ↔ (⟨π‘₯, π‘§βŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) ∈ 𝑒)))
2618, 25syl 14 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (⟨π‘₯, π‘§βŸ© ∈ (◑𝐹 β€œ 𝑒) ↔ (⟨π‘₯, π‘§βŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) ∈ 𝑒)))
27 opelxp 4658 . . . . . . . . 9 (⟨π‘₯, π‘§βŸ© ∈ (𝑋 Γ— π‘Œ) ↔ (π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ))
28 df-ov 5880 . . . . . . . . . . 11 (π‘₯𝐹𝑧) = (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©)
2928eqcomi 2181 . . . . . . . . . 10 (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) = (π‘₯𝐹𝑧)
3029eleq1i 2243 . . . . . . . . 9 ((πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) ∈ 𝑒 ↔ (π‘₯𝐹𝑧) ∈ 𝑒)
3127, 30anbi12i 460 . . . . . . . 8 ((⟨π‘₯, π‘§βŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) ∈ 𝑒) ↔ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒))
32 simprll 537 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ π‘₯ ∈ 𝑋)
33 snelpwi 4214 . . . . . . . . . . . 12 (π‘₯ ∈ 𝑋 β†’ {π‘₯} ∈ 𝒫 𝑋)
3432, 33syl 14 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ {π‘₯} ∈ 𝒫 𝑋)
3511mptpreima 5124 . . . . . . . . . . . 12 (β—‘(𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) β€œ 𝑒) = {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}
368adantrr 479 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ)) β†’ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
3736ad2ant2r 509 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ (𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
38 simplr 528 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ 𝑒 ∈ 𝐾)
39 cnima 13759 . . . . . . . . . . . . 13 (((𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) ∈ (𝐽 Cn 𝐾) ∧ 𝑒 ∈ 𝐾) β†’ (β—‘(𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) β€œ 𝑒) ∈ 𝐽)
4037, 38, 39syl2anc 411 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ (β—‘(𝑦 ∈ π‘Œ ↦ (π‘₯𝐹𝑦)) β€œ 𝑒) ∈ 𝐽)
4135, 40eqeltrrid 2265 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} ∈ 𝐽)
42 simprlr 538 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ 𝑧 ∈ π‘Œ)
43 simprr 531 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ (π‘₯𝐹𝑧) ∈ 𝑒)
44 vsnid 3626 . . . . . . . . . . . . . 14 π‘₯ ∈ {π‘₯}
45 opelxp 4658 . . . . . . . . . . . . . 14 (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ↔ (π‘₯ ∈ {π‘₯} ∧ 𝑧 ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}))
4644, 45mpbiran 940 . . . . . . . . . . . . 13 (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ↔ 𝑧 ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})
47 oveq2 5885 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 β†’ (π‘₯𝐹𝑦) = (π‘₯𝐹𝑧))
4847eleq1d 2246 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 β†’ ((π‘₯𝐹𝑦) ∈ 𝑒 ↔ (π‘₯𝐹𝑧) ∈ 𝑒))
4948elrab 2895 . . . . . . . . . . . . 13 (𝑧 ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} ↔ (𝑧 ∈ π‘Œ ∧ (π‘₯𝐹𝑧) ∈ 𝑒))
5046, 49bitri 184 . . . . . . . . . . . 12 (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ↔ (𝑧 ∈ π‘Œ ∧ (π‘₯𝐹𝑧) ∈ 𝑒))
5142, 43, 50sylanbrc 417 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ ⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}))
52 relxp 4737 . . . . . . . . . . . . 13 Rel ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})
5352a1i 9 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ Rel ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}))
54 opelxp 4658 . . . . . . . . . . . . 13 (βŸ¨π‘›, π‘šβŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ↔ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}))
5532snssd 3739 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ {π‘₯} βŠ† 𝑋)
5655sselda 3157 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ 𝑛 ∈ {π‘₯}) β†’ 𝑛 ∈ 𝑋)
5756adantrr 479 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ 𝑛 ∈ 𝑋)
58 elrabi 2892 . . . . . . . . . . . . . . . . 17 (π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ π‘š ∈ π‘Œ)
5958ad2antll 491 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ π‘š ∈ π‘Œ)
6057, 59opelxpd 4661 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ βŸ¨π‘›, π‘šβŸ© ∈ (𝑋 Γ— π‘Œ))
61 df-ov 5880 . . . . . . . . . . . . . . . . 17 (π‘›πΉπ‘š) = (πΉβ€˜βŸ¨π‘›, π‘šβŸ©)
62 elsni 3612 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ {π‘₯} β†’ 𝑛 = π‘₯)
6362ad2antrl 490 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ 𝑛 = π‘₯)
6463oveq1d 5892 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ (π‘›πΉπ‘š) = (π‘₯πΉπ‘š))
6561, 64eqtr3id 2224 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ (πΉβ€˜βŸ¨π‘›, π‘šβŸ©) = (π‘₯πΉπ‘š))
66 oveq2 5885 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = π‘š β†’ (π‘₯𝐹𝑦) = (π‘₯πΉπ‘š))
6766eleq1d 2246 . . . . . . . . . . . . . . . . . . 19 (𝑦 = π‘š β†’ ((π‘₯𝐹𝑦) ∈ 𝑒 ↔ (π‘₯πΉπ‘š) ∈ 𝑒))
6867elrab 2895 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} ↔ (π‘š ∈ π‘Œ ∧ (π‘₯πΉπ‘š) ∈ 𝑒))
6968simprbi 275 . . . . . . . . . . . . . . . . 17 (π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ (π‘₯πΉπ‘š) ∈ 𝑒)
7069ad2antll 491 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ (π‘₯πΉπ‘š) ∈ 𝑒)
7165, 70eqeltrd 2254 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ (πΉβ€˜βŸ¨π‘›, π‘šβŸ©) ∈ 𝑒)
72 elpreima 5637 . . . . . . . . . . . . . . . . 17 (𝐹 Fn (𝑋 Γ— π‘Œ) β†’ (βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒) ↔ (βŸ¨π‘›, π‘šβŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘›, π‘šβŸ©) ∈ 𝑒)))
731, 72syl 14 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒) ↔ (βŸ¨π‘›, π‘šβŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘›, π‘šβŸ©) ∈ 𝑒)))
7473ad3antrrr 492 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ (βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒) ↔ (βŸ¨π‘›, π‘šβŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘›, π‘šβŸ©) ∈ 𝑒)))
7560, 71, 74mpbir2and 944 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) ∧ (𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})) β†’ βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒))
7675ex 115 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ ((𝑛 ∈ {π‘₯} ∧ π‘š ∈ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) β†’ βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒)))
7754, 76biimtrid 152 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ (βŸ¨π‘›, π‘šβŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) β†’ βŸ¨π‘›, π‘šβŸ© ∈ (◑𝐹 β€œ 𝑒)))
7853, 77relssdv 4720 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) βŠ† (◑𝐹 β€œ 𝑒))
79 xpeq1 4642 . . . . . . . . . . . . . 14 (π‘Ž = {π‘₯} β†’ (π‘Ž Γ— 𝑏) = ({π‘₯} Γ— 𝑏))
8079eleq2d 2247 . . . . . . . . . . . . 13 (π‘Ž = {π‘₯} β†’ (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ↔ ⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— 𝑏)))
8179sseq1d 3186 . . . . . . . . . . . . 13 (π‘Ž = {π‘₯} β†’ ((π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒) ↔ ({π‘₯} Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
8280, 81anbi12d 473 . . . . . . . . . . . 12 (π‘Ž = {π‘₯} β†’ ((⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)) ↔ (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— 𝑏) ∧ ({π‘₯} Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))))
83 xpeq2 4643 . . . . . . . . . . . . . 14 (𝑏 = {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ ({π‘₯} Γ— 𝑏) = ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}))
8483eleq2d 2247 . . . . . . . . . . . . 13 (𝑏 = {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— 𝑏) ↔ ⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒})))
8583sseq1d 3186 . . . . . . . . . . . . 13 (𝑏 = {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ (({π‘₯} Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒) ↔ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) βŠ† (◑𝐹 β€œ 𝑒)))
8684, 85anbi12d 473 . . . . . . . . . . . 12 (𝑏 = {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} β†’ ((⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— 𝑏) ∧ ({π‘₯} Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)) ↔ (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ∧ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) βŠ† (◑𝐹 β€œ 𝑒))))
8782, 86rspc2ev 2858 . . . . . . . . . . 11 (({π‘₯} ∈ 𝒫 𝑋 ∧ {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒} ∈ 𝐽 ∧ (⟨π‘₯, π‘§βŸ© ∈ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) ∧ ({π‘₯} Γ— {𝑦 ∈ π‘Œ ∣ (π‘₯𝐹𝑦) ∈ 𝑒}) βŠ† (◑𝐹 β€œ 𝑒))) β†’ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
8834, 41, 51, 78, 87syl112anc 1242 . . . . . . . . . 10 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
89 vex 2742 . . . . . . . . . . . 12 π‘₯ ∈ V
90 vex 2742 . . . . . . . . . . . 12 𝑧 ∈ V
9189, 90opex 4231 . . . . . . . . . . 11 ⟨π‘₯, π‘§βŸ© ∈ V
92 eleq1 2240 . . . . . . . . . . . . 13 (𝑣 = ⟨π‘₯, π‘§βŸ© β†’ (𝑣 ∈ (π‘Ž Γ— 𝑏) ↔ ⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏)))
9392anbi1d 465 . . . . . . . . . . . 12 (𝑣 = ⟨π‘₯, π‘§βŸ© β†’ ((𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)) ↔ (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))))
94932rexbidv 2502 . . . . . . . . . . 11 (𝑣 = ⟨π‘₯, π‘§βŸ© β†’ (βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)) ↔ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))))
9591, 94elab 2883 . . . . . . . . . 10 (⟨π‘₯, π‘§βŸ© ∈ {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))} ↔ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (⟨π‘₯, π‘§βŸ© ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
9688, 95sylibr 134 . . . . . . . . 9 (((πœ‘ ∧ 𝑒 ∈ 𝐾) ∧ ((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒)) β†’ ⟨π‘₯, π‘§βŸ© ∈ {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))})
9796ex 115 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (((π‘₯ ∈ 𝑋 ∧ 𝑧 ∈ π‘Œ) ∧ (π‘₯𝐹𝑧) ∈ 𝑒) β†’ ⟨π‘₯, π‘§βŸ© ∈ {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))}))
9831, 97biimtrid 152 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ ((⟨π‘₯, π‘§βŸ© ∈ (𝑋 Γ— π‘Œ) ∧ (πΉβ€˜βŸ¨π‘₯, π‘§βŸ©) ∈ 𝑒) β†’ ⟨π‘₯, π‘§βŸ© ∈ {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))}))
9926, 98sylbid 150 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (⟨π‘₯, π‘§βŸ© ∈ (◑𝐹 β€œ 𝑒) β†’ ⟨π‘₯, π‘§βŸ© ∈ {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))}))
10024, 99relssdv 4720 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (◑𝐹 β€œ 𝑒) βŠ† {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))})
101 ssabral 3228 . . . . 5 ((◑𝐹 β€œ 𝑒) βŠ† {𝑣 ∣ βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))} ↔ βˆ€π‘£ ∈ (◑𝐹 β€œ 𝑒)βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
102100, 101sylib 122 . . . 4 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ βˆ€π‘£ ∈ (◑𝐹 β€œ 𝑒)βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒)))
103 txdis1cn.x . . . . . . 7 (πœ‘ β†’ 𝑋 ∈ 𝑉)
104 distopon 13626 . . . . . . 7 (𝑋 ∈ 𝑉 β†’ 𝒫 𝑋 ∈ (TopOnβ€˜π‘‹))
105103, 104syl 14 . . . . . 6 (πœ‘ β†’ 𝒫 𝑋 ∈ (TopOnβ€˜π‘‹))
106105adantr 276 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ 𝒫 𝑋 ∈ (TopOnβ€˜π‘‹))
1072adantr 276 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ 𝐽 ∈ (TopOnβ€˜π‘Œ))
108 eltx 13798 . . . . 5 ((𝒫 𝑋 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ (TopOnβ€˜π‘Œ)) β†’ ((◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽) ↔ βˆ€π‘£ ∈ (◑𝐹 β€œ 𝑒)βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))))
109106, 107, 108syl2anc 411 . . . 4 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ ((◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽) ↔ βˆ€π‘£ ∈ (◑𝐹 β€œ 𝑒)βˆƒπ‘Ž ∈ 𝒫 π‘‹βˆƒπ‘ ∈ 𝐽 (𝑣 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (◑𝐹 β€œ 𝑒))))
110102, 109mpbird 167 . . 3 ((πœ‘ ∧ 𝑒 ∈ 𝐾) β†’ (◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽))
111110ralrimiva 2550 . 2 (πœ‘ β†’ βˆ€π‘’ ∈ 𝐾 (◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽))
112 txtopon 13801 . . . 4 ((𝒫 𝑋 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝒫 𝑋 Γ—t 𝐽) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
113105, 2, 112syl2anc 411 . . 3 (πœ‘ β†’ (𝒫 𝑋 Γ—t 𝐽) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
114 iscn 13736 . . 3 (((𝒫 𝑋 Γ—t 𝐽) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)) ∧ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾)) β†’ (𝐹 ∈ ((𝒫 𝑋 Γ—t 𝐽) Cn 𝐾) ↔ (𝐹:(𝑋 Γ— π‘Œ)⟢βˆͺ 𝐾 ∧ βˆ€π‘’ ∈ 𝐾 (◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽))))
115113, 6, 114syl2anc 411 . 2 (πœ‘ β†’ (𝐹 ∈ ((𝒫 𝑋 Γ—t 𝐽) Cn 𝐾) ↔ (𝐹:(𝑋 Γ— π‘Œ)⟢βˆͺ 𝐾 ∧ βˆ€π‘’ ∈ 𝐾 (◑𝐹 β€œ 𝑒) ∈ (𝒫 𝑋 Γ—t 𝐽))))
11616, 111, 115mpbir2and 944 1 (πœ‘ β†’ 𝐹 ∈ ((𝒫 𝑋 Γ—t 𝐽) Cn 𝐾))
Colors of variables: wff set class
Syntax hints:   β†’ wi 4   ∧ wa 104   ↔ wb 105   = wceq 1353   ∈ wcel 2148  {cab 2163  βˆ€wral 2455  βˆƒwrex 2456  {crab 2459   βŠ† wss 3131  π’« cpw 3577  {csn 3594  βŸ¨cop 3597  βˆͺ cuni 3811   ↦ cmpt 4066   Γ— cxp 4626  β—‘ccnv 4627  dom cdm 4628   β€œ cima 4631  Rel wrel 4633   Fn wfn 5213  βŸΆwf 5214  β€˜cfv 5218  (class class class)co 5877  Topctop 13536  TopOnctopon 13549   Cn ccn 13724   Γ—t ctx 13791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-ov 5880  df-oprab 5881  df-mpo 5882  df-1st 6143  df-2nd 6144  df-map 6652  df-topgen 12714  df-top 13537  df-topon 13550  df-bases 13582  df-cn 13727  df-tx 13792
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator