Metamath Proof Explorer

Theorem cvmliftmolem2

Description: Lemma for cvmliftmo . (Contributed by Mario Carneiro, 10-Mar-2015)

Ref Expression
Hypotheses cvmliftmo.b ⊢ 𝐵 = ∪ 𝐶
cvmliftmo.y ⊢ 𝑌 = ∪ 𝐾
cvmliftmo.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
cvmliftmo.k ⊢ ( 𝜑 → 𝐾 ∈ Conn )
cvmliftmo.l ⊢ ( 𝜑 → 𝐾 ∈ 𝑛-Locally Conn )
cvmliftmo.o ⊢ ( 𝜑 → 𝑂 ∈ 𝑌 )
cvmliftmoi.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐾 Cn 𝐶 ) )
cvmliftmoi.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐾 Cn 𝐶 ) )
cvmliftmoi.g ⊢ ( 𝜑 → ( 𝐹 ∘ 𝑀 ) = ( 𝐹 ∘ 𝑁 ) )
cvmliftmoi.p ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑂 ) = ( 𝑁 ‘ 𝑂 ) )
cvmliftmolem.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
Assertion cvmliftmolem2 ( 𝜑 → 𝑀 = 𝑁 )

Proof

Step Hyp Ref Expression
1 cvmliftmo.b ⊢ 𝐵 = ∪ 𝐶
2 cvmliftmo.y ⊢ 𝑌 = ∪ 𝐾
3 cvmliftmo.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
4 cvmliftmo.k ⊢ ( 𝜑 → 𝐾 ∈ Conn )
5 cvmliftmo.l ⊢ ( 𝜑 → 𝐾 ∈ 𝑛-Locally Conn )
6 cvmliftmo.o ⊢ ( 𝜑 → 𝑂 ∈ 𝑌 )
7 cvmliftmoi.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐾 Cn 𝐶 ) )
8 cvmliftmoi.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐾 Cn 𝐶 ) )
9 cvmliftmoi.g ⊢ ( 𝜑 → ( 𝐹 ∘ 𝑀 ) = ( 𝐹 ∘ 𝑁 ) )
10 cvmliftmoi.p ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑂 ) = ( 𝑁 ‘ 𝑂 ) )
11 cvmliftmolem.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
12 2 1 cnf ⊢ ( 𝑀 ∈ ( 𝐾 Cn 𝐶 ) → 𝑀 : 𝑌 ⟶ 𝐵 )
13 ffn ⊢ ( 𝑀 : 𝑌 ⟶ 𝐵 → 𝑀 Fn 𝑌 )
14 7 12 13 3syl ⊢ ( 𝜑 → 𝑀 Fn 𝑌 )
15 2 1 cnf ⊢ ( 𝑁 ∈ ( 𝐾 Cn 𝐶 ) → 𝑁 : 𝑌 ⟶ 𝐵 )
16 ffn ⊢ ( 𝑁 : 𝑌 ⟶ 𝐵 → 𝑁 Fn 𝑌 )
17 8 15 16 3syl ⊢ ( 𝜑 → 𝑁 Fn 𝑌 )
18 inss1 ⊢ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ⊆ 𝐾
19 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
20 7 12 syl ⊢ ( 𝜑 → 𝑀 : 𝑌 ⟶ 𝐵 )
21 20 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝑀 ‘ 𝑥 ) ∈ 𝐵 )
22 cvmcn ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )
23 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
24 1 23 cnf ⊢ ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) → 𝐹 : 𝐵 ⟶ ∪ 𝐽 )
25 3 22 24 3syl ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ∪ 𝐽 )
26 25 ffvelrnda ⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑥 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ ∪ 𝐽 )
27 21 26 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ ∪ 𝐽 )
28 11 23 cvmcov ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ ∪ 𝐽 ) → ∃ 𝑎 ∈ 𝐽 ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ ( 𝑆 ‘ 𝑎 ) ≠ ∅ ) )
29 19 27 28 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ∃ 𝑎 ∈ 𝐽 ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ ( 𝑆 ‘ 𝑎 ) ≠ ∅ ) )
30 n0 ⊢ ( ( 𝑆 ‘ 𝑎 ) ≠ ∅ ↔ ∃ 𝑡 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) )
31 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) → 𝐾 ∈ 𝑛-Locally Conn )
32 7 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) → 𝑀 ∈ ( 𝐾 Cn 𝐶 ) )
33 simprrr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) → 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) )
34 11 cvmsss ⊢ ( 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) → 𝑡 ⊆ 𝐶 )
35 33 34 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) → 𝑡 ⊆ 𝐶 )
36 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
37 20 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) → 𝑀 : 𝑌 ⟶ 𝐵 )
38 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) → 𝑥 ∈ 𝑌 )
39 37 38 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) → ( 𝑀 ‘ 𝑥 ) ∈ 𝐵 )
40 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) → ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 )
41 eqid ⊢ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) = ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 )
42 11 1 41 cvmsiota ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ∧ ( 𝑀 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ) ) → ( ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ∈ 𝑡 ∧ ( 𝑀 ‘ 𝑥 ) ∈ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) )
43 36 33 39 40 42 syl13anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) → ( ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ∈ 𝑡 ∧ ( 𝑀 ‘ 𝑥 ) ∈ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) )
44 43 simpld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) → ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ∈ 𝑡 )
45 35 44 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) → ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ∈ 𝐶 )
46 cnima ⊢ ( ( 𝑀 ∈ ( 𝐾 Cn 𝐶 ) ∧ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ∈ 𝐶 ) → ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∈ 𝐾 )
47 32 45 46 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) → ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∈ 𝐾 )
48 43 simprd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) → ( 𝑀 ‘ 𝑥 ) ∈ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) )
49 elpreima ⊢ ( 𝑀 Fn 𝑌 → ( 𝑥 ∈ ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ↔ ( 𝑥 ∈ 𝑌 ∧ ( 𝑀 ‘ 𝑥 ) ∈ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ) )
50 37 13 49 3syl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) → ( 𝑥 ∈ ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ↔ ( 𝑥 ∈ 𝑌 ∧ ( 𝑀 ‘ 𝑥 ) ∈ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ) )
51 38 48 50 mpbir2and ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) → 𝑥 ∈ ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) )
52 nlly2i ⊢ ( ( 𝐾 ∈ 𝑛-Locally Conn ∧ ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∈ 𝐾 ∧ 𝑥 ∈ ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ) → ∃ 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∃ 𝑦 ∈ 𝐾 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) )
53 31 47 51 52 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) → ∃ 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∃ 𝑦 ∈ 𝐾 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) )
54 simprr1 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ) → 𝑥 ∈ 𝑦 )
55 simplrr ⊢ ( ( ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ∧ 𝑧 ∈ 𝑦 ) ) → 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) )
56 55 adantl ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ∧ 𝑧 ∈ 𝑦 ) ) ) → 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) )
57 44 adantrr ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ∧ 𝑧 ∈ 𝑦 ) ) ) → ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ∈ 𝑡 )
58 simplll ⊢ ( ( ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ∧ 𝑧 ∈ 𝑦 ) → 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) )
59 58 ad2antll ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ∧ 𝑧 ∈ 𝑦 ) ) ) → 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) )
60 59 elpwid ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ∧ 𝑧 ∈ 𝑦 ) ) ) → 𝑠 ⊆ ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) )
61 simplr3 ⊢ ( ( ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ∧ 𝑧 ∈ 𝑦 ) → ( 𝐾 ↾t 𝑠 ) ∈ Conn )
62 61 ad2antll ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ∧ 𝑧 ∈ 𝑦 ) ) ) → ( 𝐾 ↾t 𝑠 ) ∈ Conn )
63 simplr2 ⊢ ( ( ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ∧ 𝑧 ∈ 𝑦 ) → 𝑦 ⊆ 𝑠 )
64 63 ad2antll ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ∧ 𝑧 ∈ 𝑦 ) ) ) → 𝑦 ⊆ 𝑠 )
65 simprr1 ⊢ ( ( ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ) → 𝑥 ∈ 𝑦 )
66 65 adantl ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ) ) → 𝑥 ∈ 𝑦 )
67 66 adantrrr ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ∧ 𝑧 ∈ 𝑦 ) ) ) → 𝑥 ∈ 𝑦 )
68 64 67 sseldd ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ∧ 𝑧 ∈ 𝑦 ) ) ) → 𝑥 ∈ 𝑠 )
69 simprrr ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ∧ 𝑧 ∈ 𝑦 ) ) ) → 𝑧 ∈ 𝑦 )
70 64 69 sseldd ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ∧ 𝑧 ∈ 𝑦 ) ) ) → 𝑧 ∈ 𝑠 )
71 40 adantrr ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ∧ 𝑧 ∈ 𝑦 ) ) ) → ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 )
72 1 2 3 4 5 6 7 8 9 10 11 56 57 60 62 68 68 70 71 cvmliftmolem1 ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ∧ 𝑧 ∈ 𝑦 ) ) ) → ( 𝑥 ∈ dom ( 𝑀 ∩ 𝑁 ) → 𝑧 ∈ dom ( 𝑀 ∩ 𝑁 ) ) )
73 1 2 3 4 5 6 7 8 9 10 11 56 57 60 62 68 70 68 71 cvmliftmolem1 ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ∧ 𝑧 ∈ 𝑦 ) ) ) → ( 𝑧 ∈ dom ( 𝑀 ∩ 𝑁 ) → 𝑥 ∈ dom ( 𝑀 ∩ 𝑁 ) ) )
74 72 73 impbid ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ∧ 𝑧 ∈ 𝑦 ) ) ) → ( 𝑥 ∈ dom ( 𝑀 ∩ 𝑁 ) ↔ 𝑧 ∈ dom ( 𝑀 ∩ 𝑁 ) ) )
75 74 anassrs ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) ∧ ( ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ∧ 𝑧 ∈ 𝑦 ) ) → ( 𝑥 ∈ dom ( 𝑀 ∩ 𝑁 ) ↔ 𝑧 ∈ dom ( 𝑀 ∩ 𝑁 ) ) )
76 75 anassrs ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ) ∧ 𝑧 ∈ 𝑦 ) → ( 𝑥 ∈ dom ( 𝑀 ∩ 𝑁 ) ↔ 𝑧 ∈ dom ( 𝑀 ∩ 𝑁 ) ) )
77 76 ralrimiva ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ) → ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ dom ( 𝑀 ∩ 𝑁 ) ↔ 𝑧 ∈ dom ( 𝑀 ∩ 𝑁 ) ) )
78 54 77 jca ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) ) ) → ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ dom ( 𝑀 ∩ 𝑁 ) ↔ 𝑧 ∈ dom ( 𝑀 ∩ 𝑁 ) ) ) )
79 78 expr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) ∧ ( 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∧ 𝑦 ∈ 𝐾 ) ) → ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) → ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ dom ( 𝑀 ∩ 𝑁 ) ↔ 𝑧 ∈ dom ( 𝑀 ∩ 𝑁 ) ) ) ) )
80 79 anassrs ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) ∧ 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ) ∧ 𝑦 ∈ 𝐾 ) → ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) → ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ dom ( 𝑀 ∩ 𝑁 ) ↔ 𝑧 ∈ dom ( 𝑀 ∩ 𝑁 ) ) ) ) )
81 80 reximdva ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) ∧ 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ) → ( ∃ 𝑦 ∈ 𝐾 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) → ∃ 𝑦 ∈ 𝐾 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ dom ( 𝑀 ∩ 𝑁 ) ↔ 𝑧 ∈ dom ( 𝑀 ∩ 𝑁 ) ) ) ) )
82 81 rexlimdva ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) → ( ∃ 𝑠 ∈ 𝒫 ( ◡ 𝑀 “ ( ℩ 𝑏 ∈ 𝑡 ( 𝑀 ‘ 𝑥 ) ∈ 𝑏 ) ) ∃ 𝑦 ∈ 𝐾 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑠 ∧ ( 𝐾 ↾t 𝑠 ) ∈ Conn ) → ∃ 𝑦 ∈ 𝐾 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ dom ( 𝑀 ∩ 𝑁 ) ↔ 𝑧 ∈ dom ( 𝑀 ∩ 𝑁 ) ) ) ) )
83 53 82 mpd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ) → ∃ 𝑦 ∈ 𝐾 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ dom ( 𝑀 ∩ 𝑁 ) ↔ 𝑧 ∈ dom ( 𝑀 ∩ 𝑁 ) ) ) )
84 83 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ) ∧ ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) → ∃ 𝑦 ∈ 𝐾 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ dom ( 𝑀 ∩ 𝑁 ) ↔ 𝑧 ∈ dom ( 𝑀 ∩ 𝑁 ) ) ) )
85 84 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ) ∧ ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ) → ( 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) → ∃ 𝑦 ∈ 𝐾 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ dom ( 𝑀 ∩ 𝑁 ) ↔ 𝑧 ∈ dom ( 𝑀 ∩ 𝑁 ) ) ) ) )
86 85 exlimdv ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ) ∧ ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ) → ( ∃ 𝑡 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) → ∃ 𝑦 ∈ 𝐾 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ dom ( 𝑀 ∩ 𝑁 ) ↔ 𝑧 ∈ dom ( 𝑀 ∩ 𝑁 ) ) ) ) )
87 30 86 syl5bi ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ) ∧ ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ) → ( ( 𝑆 ‘ 𝑎 ) ≠ ∅ → ∃ 𝑦 ∈ 𝐾 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ dom ( 𝑀 ∩ 𝑁 ) ↔ 𝑧 ∈ dom ( 𝑀 ∩ 𝑁 ) ) ) ) )
88 87 expimpd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝐽 ) ) → ( ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ ( 𝑆 ‘ 𝑎 ) ≠ ∅ ) → ∃ 𝑦 ∈ 𝐾 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ dom ( 𝑀 ∩ 𝑁 ) ↔ 𝑧 ∈ dom ( 𝑀 ∩ 𝑁 ) ) ) ) )
89 88 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑎 ∈ 𝐽 ) → ( ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ ( 𝑆 ‘ 𝑎 ) ≠ ∅ ) → ∃ 𝑦 ∈ 𝐾 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ dom ( 𝑀 ∩ 𝑁 ) ↔ 𝑧 ∈ dom ( 𝑀 ∩ 𝑁 ) ) ) ) )
90 89 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ∃ 𝑎 ∈ 𝐽 ( ( 𝐹 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ 𝑎 ∧ ( 𝑆 ‘ 𝑎 ) ≠ ∅ ) → ∃ 𝑦 ∈ 𝐾 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ dom ( 𝑀 ∩ 𝑁 ) ↔ 𝑧 ∈ dom ( 𝑀 ∩ 𝑁 ) ) ) ) )
91 29 90 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ∃ 𝑦 ∈ 𝐾 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ dom ( 𝑀 ∩ 𝑁 ) ↔ 𝑧 ∈ dom ( 𝑀 ∩ 𝑁 ) ) ) )
92 91 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑌 ∃ 𝑦 ∈ 𝐾 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ dom ( 𝑀 ∩ 𝑁 ) ↔ 𝑧 ∈ dom ( 𝑀 ∩ 𝑁 ) ) ) )
93 conntop ⊢ ( 𝐾 ∈ Conn → 𝐾 ∈ Top )
94 4 93 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
95 fndmin ⊢ ( ( 𝑀 Fn 𝑌 ∧ 𝑁 Fn 𝑌 ) → dom ( 𝑀 ∩ 𝑁 ) = { 𝑥 ∈ 𝑌 ∣ ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) } )
96 14 17 95 syl2anc ⊢ ( 𝜑 → dom ( 𝑀 ∩ 𝑁 ) = { 𝑥 ∈ 𝑌 ∣ ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) } )
97 ssrab2 ⊢ { 𝑥 ∈ 𝑌 ∣ ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) } ⊆ 𝑌
98 96 97 eqsstrdi ⊢ ( 𝜑 → dom ( 𝑀 ∩ 𝑁 ) ⊆ 𝑌 )
99 2 isclo ⊢ ( ( 𝐾 ∈ Top ∧ dom ( 𝑀 ∩ 𝑁 ) ⊆ 𝑌 ) → ( dom ( 𝑀 ∩ 𝑁 ) ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ↔ ∀ 𝑥 ∈ 𝑌 ∃ 𝑦 ∈ 𝐾 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ dom ( 𝑀 ∩ 𝑁 ) ↔ 𝑧 ∈ dom ( 𝑀 ∩ 𝑁 ) ) ) ) )
100 94 98 99 syl2anc ⊢ ( 𝜑 → ( dom ( 𝑀 ∩ 𝑁 ) ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ↔ ∀ 𝑥 ∈ 𝑌 ∃ 𝑦 ∈ 𝐾 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑥 ∈ dom ( 𝑀 ∩ 𝑁 ) ↔ 𝑧 ∈ dom ( 𝑀 ∩ 𝑁 ) ) ) ) )
101 92 100 mpbird ⊢ ( 𝜑 → dom ( 𝑀 ∩ 𝑁 ) ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) )
102 18 101 sselid ⊢ ( 𝜑 → dom ( 𝑀 ∩ 𝑁 ) ∈ 𝐾 )
103 fveq2 ⊢ ( 𝑥 = 𝑂 → ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑂 ) )
104 fveq2 ⊢ ( 𝑥 = 𝑂 → ( 𝑁 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑂 ) )
105 103 104 eqeq12d ⊢ ( 𝑥 = 𝑂 → ( ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑀 ‘ 𝑂 ) = ( 𝑁 ‘ 𝑂 ) ) )
106 105 elrab ⊢ ( 𝑂 ∈ { 𝑥 ∈ 𝑌 ∣ ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) } ↔ ( 𝑂 ∈ 𝑌 ∧ ( 𝑀 ‘ 𝑂 ) = ( 𝑁 ‘ 𝑂 ) ) )
107 6 10 106 sylanbrc ⊢ ( 𝜑 → 𝑂 ∈ { 𝑥 ∈ 𝑌 ∣ ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) } )
108 107 96 eleqtrrd ⊢ ( 𝜑 → 𝑂 ∈ dom ( 𝑀 ∩ 𝑁 ) )
109 108 ne0d ⊢ ( 𝜑 → dom ( 𝑀 ∩ 𝑁 ) ≠ ∅ )
110 inss2 ⊢ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ⊆ ( Clsd ‘ 𝐾 )
111 110 101 sselid ⊢ ( 𝜑 → dom ( 𝑀 ∩ 𝑁 ) ∈ ( Clsd ‘ 𝐾 ) )
112 2 4 102 109 111 connclo ⊢ ( 𝜑 → dom ( 𝑀 ∩ 𝑁 ) = 𝑌 )
113 112 96 eqtr3d ⊢ ( 𝜑 → 𝑌 = { 𝑥 ∈ 𝑌 ∣ ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) } )
114 rabid2 ⊢ ( 𝑌 = { 𝑥 ∈ 𝑌 ∣ ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) } ↔ ∀ 𝑥 ∈ 𝑌 ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) )
115 113 114 sylib ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑌 ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) )
116 115 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) )
117 14 17 116 eqfnfvd ⊢ ( 𝜑 → 𝑀 = 𝑁 )