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 S = k J s 𝒫 C | s = F -1 k u s v s u u v = F u C 𝑡 u Homeo J 𝑡 k
cvmseu.1 B = C
Assertion cvmseu F C CovMap J T S U A B F A U ∃! x T A x

Proof

Step Hyp Ref Expression
1 cvmcov.1 S = k J s 𝒫 C | s = F -1 k u s v s u u v = F u C 𝑡 u Homeo J 𝑡 k
2 cvmseu.1 B = C
3 simpr2 F C CovMap J T S U A B F A U A B
4 simpr3 F C CovMap J T S U A B F A U F A U
5 cvmcn F C CovMap J F C Cn J
6 5 adantr F C CovMap J T S U A B F A U F C Cn J
7 eqid J = J
8 2 7 cnf F C Cn J F : B J
9 ffn F : B J F Fn B
10 elpreima F Fn B A F -1 U A B F A U
11 6 8 9 10 4syl F C CovMap J T S U A B F A U A F -1 U A B F A U
12 3 4 11 mpbir2and F C CovMap J T S U A B F A U A F -1 U
13 simpr1 F C CovMap J T S U A B F A U T S U
14 1 cvmsuni T S U T = F -1 U
15 13 14 syl F C CovMap J T S U A B F A U T = F -1 U
16 12 15 eleqtrrd F C CovMap J T S U A B F A U A T
17 eluni2 A T x T A x
18 16 17 sylib F C CovMap J T S U A B F A U x T A x
19 inelcm A x A z x z
20 1 cvmsdisj T S U x T z T x = z x z =
21 20 3expb T S U x T z T x = z x z =
22 13 21 sylan F C CovMap J T S U A B F A U x T z T x = z x z =
23 22 ord F C CovMap J T S U A B F A U x T z T ¬ x = z x z =
24 23 necon1ad F C CovMap J T S U A B F A U x T z T x z x = z
25 19 24 syl5 F C CovMap J T S U A B F A U x T z T A x A z x = z
26 25 ralrimivva F C CovMap J T S U A B F A U x T z T A x A z x = z
27 eleq2w x = z A x A z
28 27 reu4 ∃! x T A x x T A x x T z T A x A z x = z
29 18 26 28 sylanbrc F C CovMap J T S U A B F A U ∃! x T A x