Metamath Proof Explorer

Theorem cvmseu

Description: Every element in U. T is a member of a unique element of T . (Contributed by Mario Carneiro, 14-Feb-2015)

Ref Expression
Hypotheses cvmcov.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
cvmseu.1 ⊢ 𝐵 = ∪ 𝐶
Assertion cvmseu ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ) ) → ∃! 𝑥 ∈ 𝑇 𝐴 ∈ 𝑥 )

Proof

Step Hyp Ref Expression
1 cvmcov.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
2 cvmseu.1 ⊢ 𝐵 = ∪ 𝐶
3 simpr2 ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ) ) → 𝐴 ∈ 𝐵 )
4 simpr3 ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 )
5 cvmcn ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )
6 5 adantr ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ) ) → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )
7 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
8 2 7 cnf ⊢ ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) → 𝐹 : 𝐵 ⟶ ∪ 𝐽 )
9 ffn ⊢ ( 𝐹 : 𝐵 ⟶ ∪ 𝐽 → 𝐹 Fn 𝐵 )
10 elpreima ⊢ ( 𝐹 Fn 𝐵 → ( 𝐴 ∈ ( ◡ 𝐹 “ 𝑈 ) ↔ ( 𝐴 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ) ) )
11 6 8 9 10 4syl ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ) ) → ( 𝐴 ∈ ( ◡ 𝐹 “ 𝑈 ) ↔ ( 𝐴 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ) ) )
12 3 4 11 mpbir2and ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ) ) → 𝐴 ∈ ( ◡ 𝐹 “ 𝑈 ) )
13 simpr1 ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ) ) → 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) )
14 1 cvmsuni ⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → ∪ 𝑇 = ( ◡ 𝐹 “ 𝑈 ) )
15 13 14 syl ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ) ) → ∪ 𝑇 = ( ◡ 𝐹 “ 𝑈 ) )
16 12 15 eleqtrrd ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ) ) → 𝐴 ∈ ∪ 𝑇 )
17 eluni2 ⊢ ( 𝐴 ∈ ∪ 𝑇 ↔ ∃ 𝑥 ∈ 𝑇 𝐴 ∈ 𝑥 )
18 16 17 sylib ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ) ) → ∃ 𝑥 ∈ 𝑇 𝐴 ∈ 𝑥 )
19 inelcm ⊢ ( ( 𝐴 ∈ 𝑥 ∧ 𝐴 ∈ 𝑧 ) → ( 𝑥 ∩ 𝑧 ) ≠ ∅ )
20 1 cvmsdisj ⊢ ( ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝑥 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) → ( 𝑥 = 𝑧 ∨ ( 𝑥 ∩ 𝑧 ) = ∅ ) )
21 20 3expb ⊢ ( ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ ( 𝑥 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝑥 = 𝑧 ∨ ( 𝑥 ∩ 𝑧 ) = ∅ ) )
22 13 21 sylan ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ) ) ∧ ( 𝑥 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝑥 = 𝑧 ∨ ( 𝑥 ∩ 𝑧 ) = ∅ ) )
23 22 ord ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ) ) ∧ ( 𝑥 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ¬ 𝑥 = 𝑧 → ( 𝑥 ∩ 𝑧 ) = ∅ ) )
24 23 necon1ad ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ) ) ∧ ( 𝑥 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝑥 ∩ 𝑧 ) ≠ ∅ → 𝑥 = 𝑧 ) )
25 19 24 syl5 ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ) ) ∧ ( 𝑥 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝐴 ∈ 𝑥 ∧ 𝐴 ∈ 𝑧 ) → 𝑥 = 𝑧 ) )
26 25 ralrimivva ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ) ) → ∀ 𝑥 ∈ 𝑇 ∀ 𝑧 ∈ 𝑇 ( ( 𝐴 ∈ 𝑥 ∧ 𝐴 ∈ 𝑧 ) → 𝑥 = 𝑧 ) )
27 eleq2w ⊢ ( 𝑥 = 𝑧 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑧 ) )
28 27 reu4 ⊢ ( ∃! 𝑥 ∈ 𝑇 𝐴 ∈ 𝑥 ↔ ( ∃ 𝑥 ∈ 𝑇 𝐴 ∈ 𝑥 ∧ ∀ 𝑥 ∈ 𝑇 ∀ 𝑧 ∈ 𝑇 ( ( 𝐴 ∈ 𝑥 ∧ 𝐴 ∈ 𝑧 ) → 𝑥 = 𝑧 ) ) )
29 18 26 28 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ) ) → ∃! 𝑥 ∈ 𝑇 𝐴 ∈ 𝑥 )