Metamath Proof Explorer


Theorem txdis1cn

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)

Ref Expression
Hypotheses txdis1cn.x ( 𝜑𝑋𝑉 )
txdis1cn.j ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑌 ) )
txdis1cn.k ( 𝜑𝐾 ∈ Top )
txdis1cn.f ( 𝜑𝐹 Fn ( 𝑋 × 𝑌 ) )
txdis1cn.1 ( ( 𝜑𝑥𝑋 ) → ( 𝑦𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) ∈ ( 𝐽 Cn 𝐾 ) )
Assertion txdis1cn ( 𝜑𝐹 ∈ ( ( 𝒫 𝑋 ×t 𝐽 ) Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 txdis1cn.x ( 𝜑𝑋𝑉 )
2 txdis1cn.j ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑌 ) )
3 txdis1cn.k ( 𝜑𝐾 ∈ Top )
4 txdis1cn.f ( 𝜑𝐹 Fn ( 𝑋 × 𝑌 ) )
5 txdis1cn.1 ( ( 𝜑𝑥𝑋 ) → ( 𝑦𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) ∈ ( 𝐽 Cn 𝐾 ) )
6 2 adantr ( ( 𝜑𝑥𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑌 ) )
7 toptopon2 ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝐾 ) )
8 3 7 sylib ( 𝜑𝐾 ∈ ( TopOn ‘ 𝐾 ) )
9 8 adantr ( ( 𝜑𝑥𝑋 ) → 𝐾 ∈ ( TopOn ‘ 𝐾 ) )
10 cnf2 ( ( 𝐽 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝐾 ) ∧ ( 𝑦𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝑦𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) : 𝑌 𝐾 )
11 6 9 5 10 syl3anc ( ( 𝜑𝑥𝑋 ) → ( 𝑦𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) : 𝑌 𝐾 )
12 eqid ( 𝑦𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) = ( 𝑦𝑌 ↦ ( 𝑥 𝐹 𝑦 ) )
13 12 fmpt ( ∀ 𝑦𝑌 ( 𝑥 𝐹 𝑦 ) ∈ 𝐾 ↔ ( 𝑦𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) : 𝑌 𝐾 )
14 11 13 sylibr ( ( 𝜑𝑥𝑋 ) → ∀ 𝑦𝑌 ( 𝑥 𝐹 𝑦 ) ∈ 𝐾 )
15 14 ralrimiva ( 𝜑 → ∀ 𝑥𝑋𝑦𝑌 ( 𝑥 𝐹 𝑦 ) ∈ 𝐾 )
16 ffnov ( 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝐾 ↔ ( 𝐹 Fn ( 𝑋 × 𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑌 ( 𝑥 𝐹 𝑦 ) ∈ 𝐾 ) )
17 4 15 16 sylanbrc ( 𝜑𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝐾 )
18 cnvimass ( 𝐹𝑢 ) ⊆ dom 𝐹
19 4 adantr ( ( 𝜑𝑢𝐾 ) → 𝐹 Fn ( 𝑋 × 𝑌 ) )
20 19 fndmd ( ( 𝜑𝑢𝐾 ) → dom 𝐹 = ( 𝑋 × 𝑌 ) )
21 18 20 sseqtrid ( ( 𝜑𝑢𝐾 ) → ( 𝐹𝑢 ) ⊆ ( 𝑋 × 𝑌 ) )
22 relxp Rel ( 𝑋 × 𝑌 )
23 relss ( ( 𝐹𝑢 ) ⊆ ( 𝑋 × 𝑌 ) → ( Rel ( 𝑋 × 𝑌 ) → Rel ( 𝐹𝑢 ) ) )
24 21 22 23 mpisyl ( ( 𝜑𝑢𝐾 ) → Rel ( 𝐹𝑢 ) )
25 elpreima ( 𝐹 Fn ( 𝑋 × 𝑌 ) → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐹𝑢 ) ↔ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑧 ⟩ ) ∈ 𝑢 ) ) )
26 19 25 syl ( ( 𝜑𝑢𝐾 ) → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐹𝑢 ) ↔ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑧 ⟩ ) ∈ 𝑢 ) ) )
27 opelxp ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑋 × 𝑌 ) ↔ ( 𝑥𝑋𝑧𝑌 ) )
28 df-ov ( 𝑥 𝐹 𝑧 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑧 ⟩ )
29 28 eqcomi ( 𝐹 ‘ ⟨ 𝑥 , 𝑧 ⟩ ) = ( 𝑥 𝐹 𝑧 )
30 29 eleq1i ( ( 𝐹 ‘ ⟨ 𝑥 , 𝑧 ⟩ ) ∈ 𝑢 ↔ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 )
31 27 30 anbi12i ( ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑧 ⟩ ) ∈ 𝑢 ) ↔ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) )
32 simprll ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → 𝑥𝑋 )
33 snelpwi ( 𝑥𝑋 → { 𝑥 } ∈ 𝒫 𝑋 )
34 32 33 syl ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → { 𝑥 } ∈ 𝒫 𝑋 )
35 12 mptpreima ( ( 𝑦𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) “ 𝑢 ) = { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 }
36 5 adantrr ( ( 𝜑 ∧ ( 𝑥𝑋𝑧𝑌 ) ) → ( 𝑦𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) ∈ ( 𝐽 Cn 𝐾 ) )
37 36 ad2ant2r ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → ( 𝑦𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) ∈ ( 𝐽 Cn 𝐾 ) )
38 simplr ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → 𝑢𝐾 )
39 cnima ( ( ( 𝑦𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑢𝐾 ) → ( ( 𝑦𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) “ 𝑢 ) ∈ 𝐽 )
40 37 38 39 syl2anc ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → ( ( 𝑦𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) “ 𝑢 ) ∈ 𝐽 )
41 35 40 eqeltrrid ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ∈ 𝐽 )
42 simprlr ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → 𝑧𝑌 )
43 simprr ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 )
44 vsnid 𝑥 ∈ { 𝑥 }
45 opelxp ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( { 𝑥 } × { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ↔ ( 𝑥 ∈ { 𝑥 } ∧ 𝑧 ∈ { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) )
46 44 45 mpbiran ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( { 𝑥 } × { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ↔ 𝑧 ∈ { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } )
47 oveq2 ( 𝑦 = 𝑧 → ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐹 𝑧 ) )
48 47 eleq1d ( 𝑦 = 𝑧 → ( ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 ↔ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) )
49 48 elrab ( 𝑧 ∈ { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ↔ ( 𝑧𝑌 ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) )
50 46 49 bitri ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( { 𝑥 } × { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ↔ ( 𝑧𝑌 ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) )
51 42 43 50 sylanbrc ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ ( { 𝑥 } × { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) )
52 relxp Rel ( { 𝑥 } × { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } )
53 52 a1i ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → Rel ( { 𝑥 } × { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) )
54 opelxp ( ⟨ 𝑛 , 𝑚 ⟩ ∈ ( { 𝑥 } × { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ↔ ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) )
55 32 snssd ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → { 𝑥 } ⊆ 𝑋 )
56 55 sselda ( ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) ∧ 𝑛 ∈ { 𝑥 } ) → 𝑛𝑋 )
57 56 adantrr ( ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) ∧ ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ) → 𝑛𝑋 )
58 elrabi ( 𝑚 ∈ { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } → 𝑚𝑌 )
59 58 ad2antll ( ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) ∧ ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ) → 𝑚𝑌 )
60 57 59 opelxpd ( ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) ∧ ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ) → ⟨ 𝑛 , 𝑚 ⟩ ∈ ( 𝑋 × 𝑌 ) )
61 df-ov ( 𝑛 𝐹 𝑚 ) = ( 𝐹 ‘ ⟨ 𝑛 , 𝑚 ⟩ )
62 elsni ( 𝑛 ∈ { 𝑥 } → 𝑛 = 𝑥 )
63 62 ad2antrl ( ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) ∧ ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ) → 𝑛 = 𝑥 )
64 63 oveq1d ( ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) ∧ ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ) → ( 𝑛 𝐹 𝑚 ) = ( 𝑥 𝐹 𝑚 ) )
65 61 64 eqtr3id ( ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) ∧ ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ) → ( 𝐹 ‘ ⟨ 𝑛 , 𝑚 ⟩ ) = ( 𝑥 𝐹 𝑚 ) )
66 oveq2 ( 𝑦 = 𝑚 → ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐹 𝑚 ) )
67 66 eleq1d ( 𝑦 = 𝑚 → ( ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 ↔ ( 𝑥 𝐹 𝑚 ) ∈ 𝑢 ) )
68 67 elrab ( 𝑚 ∈ { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ↔ ( 𝑚𝑌 ∧ ( 𝑥 𝐹 𝑚 ) ∈ 𝑢 ) )
69 68 simprbi ( 𝑚 ∈ { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } → ( 𝑥 𝐹 𝑚 ) ∈ 𝑢 )
70 69 ad2antll ( ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) ∧ ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ) → ( 𝑥 𝐹 𝑚 ) ∈ 𝑢 )
71 65 70 eqeltrd ( ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) ∧ ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ) → ( 𝐹 ‘ ⟨ 𝑛 , 𝑚 ⟩ ) ∈ 𝑢 )
72 elpreima ( 𝐹 Fn ( 𝑋 × 𝑌 ) → ( ⟨ 𝑛 , 𝑚 ⟩ ∈ ( 𝐹𝑢 ) ↔ ( ⟨ 𝑛 , 𝑚 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ( 𝐹 ‘ ⟨ 𝑛 , 𝑚 ⟩ ) ∈ 𝑢 ) ) )
73 4 72 syl ( 𝜑 → ( ⟨ 𝑛 , 𝑚 ⟩ ∈ ( 𝐹𝑢 ) ↔ ( ⟨ 𝑛 , 𝑚 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ( 𝐹 ‘ ⟨ 𝑛 , 𝑚 ⟩ ) ∈ 𝑢 ) ) )
74 73 ad3antrrr ( ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) ∧ ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ) → ( ⟨ 𝑛 , 𝑚 ⟩ ∈ ( 𝐹𝑢 ) ↔ ( ⟨ 𝑛 , 𝑚 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ( 𝐹 ‘ ⟨ 𝑛 , 𝑚 ⟩ ) ∈ 𝑢 ) ) )
75 60 71 74 mpbir2and ( ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) ∧ ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ) → ⟨ 𝑛 , 𝑚 ⟩ ∈ ( 𝐹𝑢 ) )
76 75 ex ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → ( ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) → ⟨ 𝑛 , 𝑚 ⟩ ∈ ( 𝐹𝑢 ) ) )
77 54 76 syl5bi ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → ( ⟨ 𝑛 , 𝑚 ⟩ ∈ ( { 𝑥 } × { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) → ⟨ 𝑛 , 𝑚 ⟩ ∈ ( 𝐹𝑢 ) ) )
78 53 77 relssdv ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → ( { 𝑥 } × { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ⊆ ( 𝐹𝑢 ) )
79 xpeq1 ( 𝑎 = { 𝑥 } → ( 𝑎 × 𝑏 ) = ( { 𝑥 } × 𝑏 ) )
80 79 eleq2d ( 𝑎 = { 𝑥 } → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑎 × 𝑏 ) ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( { 𝑥 } × 𝑏 ) ) )
81 79 sseq1d ( 𝑎 = { 𝑥 } → ( ( 𝑎 × 𝑏 ) ⊆ ( 𝐹𝑢 ) ↔ ( { 𝑥 } × 𝑏 ) ⊆ ( 𝐹𝑢 ) ) )
82 80 81 anbi12d ( 𝑎 = { 𝑥 } → ( ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐹𝑢 ) ) ↔ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( { 𝑥 } × 𝑏 ) ∧ ( { 𝑥 } × 𝑏 ) ⊆ ( 𝐹𝑢 ) ) ) )
83 xpeq2 ( 𝑏 = { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } → ( { 𝑥 } × 𝑏 ) = ( { 𝑥 } × { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) )
84 83 eleq2d ( 𝑏 = { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( { 𝑥 } × 𝑏 ) ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( { 𝑥 } × { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ) )
85 83 sseq1d ( 𝑏 = { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } → ( ( { 𝑥 } × 𝑏 ) ⊆ ( 𝐹𝑢 ) ↔ ( { 𝑥 } × { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ⊆ ( 𝐹𝑢 ) ) )
86 84 85 anbi12d ( 𝑏 = { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } → ( ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( { 𝑥 } × 𝑏 ) ∧ ( { 𝑥 } × 𝑏 ) ⊆ ( 𝐹𝑢 ) ) ↔ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( { 𝑥 } × { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ∧ ( { 𝑥 } × { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ⊆ ( 𝐹𝑢 ) ) ) )
87 82 86 rspc2ev ( ( { 𝑥 } ∈ 𝒫 𝑋 ∧ { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ∈ 𝐽 ∧ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( { 𝑥 } × { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ∧ ( { 𝑥 } × { 𝑦𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ⊆ ( 𝐹𝑢 ) ) ) → ∃ 𝑎 ∈ 𝒫 𝑋𝑏𝐽 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐹𝑢 ) ) )
88 34 41 51 78 87 syl112anc ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → ∃ 𝑎 ∈ 𝒫 𝑋𝑏𝐽 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐹𝑢 ) ) )
89 opex 𝑥 , 𝑧 ⟩ ∈ V
90 eleq1 ( 𝑣 = ⟨ 𝑥 , 𝑧 ⟩ → ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑎 × 𝑏 ) ) )
91 90 anbi1d ( 𝑣 = ⟨ 𝑥 , 𝑧 ⟩ → ( ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐹𝑢 ) ) ↔ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐹𝑢 ) ) ) )
92 91 2rexbidv ( 𝑣 = ⟨ 𝑥 , 𝑧 ⟩ → ( ∃ 𝑎 ∈ 𝒫 𝑋𝑏𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐹𝑢 ) ) ↔ ∃ 𝑎 ∈ 𝒫 𝑋𝑏𝐽 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐹𝑢 ) ) ) )
93 89 92 elab ( ⟨ 𝑥 , 𝑧 ⟩ ∈ { 𝑣 ∣ ∃ 𝑎 ∈ 𝒫 𝑋𝑏𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐹𝑢 ) ) } ↔ ∃ 𝑎 ∈ 𝒫 𝑋𝑏𝐽 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐹𝑢 ) ) )
94 88 93 sylibr ( ( ( 𝜑𝑢𝐾 ) ∧ ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ { 𝑣 ∣ ∃ 𝑎 ∈ 𝒫 𝑋𝑏𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐹𝑢 ) ) } )
95 94 ex ( ( 𝜑𝑢𝐾 ) → ( ( ( 𝑥𝑋𝑧𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ { 𝑣 ∣ ∃ 𝑎 ∈ 𝒫 𝑋𝑏𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐹𝑢 ) ) } ) )
96 31 95 syl5bi ( ( 𝜑𝑢𝐾 ) → ( ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑧 ⟩ ) ∈ 𝑢 ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ { 𝑣 ∣ ∃ 𝑎 ∈ 𝒫 𝑋𝑏𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐹𝑢 ) ) } ) )
97 26 96 sylbid ( ( 𝜑𝑢𝐾 ) → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐹𝑢 ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ { 𝑣 ∣ ∃ 𝑎 ∈ 𝒫 𝑋𝑏𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐹𝑢 ) ) } ) )
98 24 97 relssdv ( ( 𝜑𝑢𝐾 ) → ( 𝐹𝑢 ) ⊆ { 𝑣 ∣ ∃ 𝑎 ∈ 𝒫 𝑋𝑏𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐹𝑢 ) ) } )
99 ssabral ( ( 𝐹𝑢 ) ⊆ { 𝑣 ∣ ∃ 𝑎 ∈ 𝒫 𝑋𝑏𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐹𝑢 ) ) } ↔ ∀ 𝑣 ∈ ( 𝐹𝑢 ) ∃ 𝑎 ∈ 𝒫 𝑋𝑏𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐹𝑢 ) ) )
100 98 99 sylib ( ( 𝜑𝑢𝐾 ) → ∀ 𝑣 ∈ ( 𝐹𝑢 ) ∃ 𝑎 ∈ 𝒫 𝑋𝑏𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐹𝑢 ) ) )
101 distopon ( 𝑋𝑉 → 𝒫 𝑋 ∈ ( TopOn ‘ 𝑋 ) )
102 1 101 syl ( 𝜑 → 𝒫 𝑋 ∈ ( TopOn ‘ 𝑋 ) )
103 102 adantr ( ( 𝜑𝑢𝐾 ) → 𝒫 𝑋 ∈ ( TopOn ‘ 𝑋 ) )
104 2 adantr ( ( 𝜑𝑢𝐾 ) → 𝐽 ∈ ( TopOn ‘ 𝑌 ) )
105 eltx ( ( 𝒫 𝑋 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ ( TopOn ‘ 𝑌 ) ) → ( ( 𝐹𝑢 ) ∈ ( 𝒫 𝑋 ×t 𝐽 ) ↔ ∀ 𝑣 ∈ ( 𝐹𝑢 ) ∃ 𝑎 ∈ 𝒫 𝑋𝑏𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐹𝑢 ) ) ) )
106 103 104 105 syl2anc ( ( 𝜑𝑢𝐾 ) → ( ( 𝐹𝑢 ) ∈ ( 𝒫 𝑋 ×t 𝐽 ) ↔ ∀ 𝑣 ∈ ( 𝐹𝑢 ) ∃ 𝑎 ∈ 𝒫 𝑋𝑏𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐹𝑢 ) ) ) )
107 100 106 mpbird ( ( 𝜑𝑢𝐾 ) → ( 𝐹𝑢 ) ∈ ( 𝒫 𝑋 ×t 𝐽 ) )
108 107 ralrimiva ( 𝜑 → ∀ 𝑢𝐾 ( 𝐹𝑢 ) ∈ ( 𝒫 𝑋 ×t 𝐽 ) )
109 txtopon ( ( 𝒫 𝑋 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝒫 𝑋 ×t 𝐽 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
110 102 2 109 syl2anc ( 𝜑 → ( 𝒫 𝑋 ×t 𝐽 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
111 iscn ( ( ( 𝒫 𝑋 ×t 𝐽 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐾 ∈ ( TopOn ‘ 𝐾 ) ) → ( 𝐹 ∈ ( ( 𝒫 𝑋 ×t 𝐽 ) Cn 𝐾 ) ↔ ( 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝐾 ∧ ∀ 𝑢𝐾 ( 𝐹𝑢 ) ∈ ( 𝒫 𝑋 ×t 𝐽 ) ) ) )
112 110 8 111 syl2anc ( 𝜑 → ( 𝐹 ∈ ( ( 𝒫 𝑋 ×t 𝐽 ) Cn 𝐾 ) ↔ ( 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝐾 ∧ ∀ 𝑢𝐾 ( 𝐹𝑢 ) ∈ ( 𝒫 𝑋 ×t 𝐽 ) ) ) )
113 17 108 112 mpbir2and ( 𝜑𝐹 ∈ ( ( 𝒫 𝑋 ×t 𝐽 ) Cn 𝐾 ) )