Metamath Proof Explorer


Theorem disjf1o

Description: A bijection built from disjoint sets. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses disjf1o.xph x φ
disjf1o.f F = x A B
disjf1o.b φ x A B V
disjf1o.dj φ Disj x A B
disjf1o.d C = x A | B
disjf1o.e D = ran F
Assertion disjf1o φ F C : C 1-1 onto D

Proof

Step Hyp Ref Expression
1 disjf1o.xph x φ
2 disjf1o.f F = x A B
3 disjf1o.b φ x A B V
4 disjf1o.dj φ Disj x A B
5 disjf1o.d C = x A | B
6 disjf1o.e D = ran F
7 eqid x C B = x C B
8 simpl φ x C φ
9 ssrab2 x A | B A
10 5 9 eqsstri C A
11 id x C x C
12 10 11 sseldi x C x A
13 12 adantl φ x C x A
14 8 13 3 syl2anc φ x C B V
15 11 5 eleqtrdi x C x x A | B
16 rabid x x A | B x A B
17 16 a1i x C x x A | B x A B
18 15 17 mpbid x C x A B
19 18 simprd x C B
20 19 adantl φ x C B
21 10 a1i φ C A
22 disjss1 C A Disj x A B Disj x C B
23 21 4 22 sylc φ Disj x C B
24 1 7 14 20 23 disjf1 φ x C B : C 1-1 V
25 f1f1orn x C B : C 1-1 V x C B : C 1-1 onto ran x C B
26 24 25 syl φ x C B : C 1-1 onto ran x C B
27 2 a1i φ F = x A B
28 27 reseq1d φ F C = x A B C
29 21 resmptd φ x A B C = x C B
30 28 29 eqtrd φ F C = x C B
31 eqidd φ C = C
32 simpl φ y D φ
33 id y D y D
34 33 6 eleqtrdi y D y ran F
35 eldifsni y ran F y
36 34 35 syl y D y
37 36 adantl φ y D y
38 eldifi y ran F y ran F
39 34 38 syl y D y ran F
40 2 elrnmpt y ran F y ran F x A y = B
41 39 40 syl y D y ran F x A y = B
42 39 41 mpbid y D x A y = B
43 42 adantl φ y D x A y = B
44 nfv x y
45 1 44 nfan x φ y
46 nfcv _ x y
47 nfmpt1 _ x x C B
48 47 nfrn _ x ran x C B
49 46 48 nfel x y ran x C B
50 simp3 y x A y = B y = B
51 simp2 y x A y = B x A
52 id y = B y = B
53 52 eqcomd y = B B = y
54 53 adantl y y = B B = y
55 simpl y y = B y
56 54 55 eqnetrd y y = B B
57 56 3adant2 y x A y = B B
58 51 57 jca y x A y = B x A B
59 58 16 sylibr y x A y = B x x A | B
60 5 eqcomi x A | B = C
61 60 a1i y x A y = B x A | B = C
62 59 61 eleqtrd y x A y = B x C
63 eqvisset y = B B V
64 63 3ad2ant3 y x A y = B B V
65 7 elrnmpt1 x C B V B ran x C B
66 62 64 65 syl2anc y x A y = B B ran x C B
67 50 66 eqeltrd y x A y = B y ran x C B
68 67 3adant1l φ y x A y = B y ran x C B
69 68 3exp φ y x A y = B y ran x C B
70 45 49 69 rexlimd φ y x A y = B y ran x C B
71 70 imp φ y x A y = B y ran x C B
72 32 37 43 71 syl21anc φ y D y ran x C B
73 72 ralrimiva φ y D y ran x C B
74 dfss3 D ran x C B y D y ran x C B
75 73 74 sylibr φ D ran x C B
76 simpl φ y ran x C B φ
77 vex y V
78 7 elrnmpt y V y ran x C B x C y = B
79 77 78 ax-mp y ran x C B x C y = B
80 79 biimpi y ran x C B x C y = B
81 80 adantl φ y ran x C B x C y = B
82 nfv x y D
83 simpr x C y = B y = B
84 12 adantr x C y = B x A
85 83 63 syl x C y = B B V
86 2 elrnmpt1 x A B V B ran F
87 84 85 86 syl2anc x C y = B B ran F
88 83 87 eqeltrd x C y = B y ran F
89 88 3adant1 φ x C y = B y ran F
90 19 adantr x C y = B B
91 83 90 eqnetrd x C y = B y
92 nelsn y ¬ y
93 91 92 syl x C y = B ¬ y
94 93 3adant1 φ x C y = B ¬ y
95 89 94 eldifd φ x C y = B y ran F
96 95 6 eleqtrrdi φ x C y = B y D
97 96 3exp φ x C y = B y D
98 1 82 97 rexlimd φ x C y = B y D
99 98 imp φ x C y = B y D
100 76 81 99 syl2anc φ y ran x C B y D
101 75 100 eqelssd φ D = ran x C B
102 30 31 101 f1oeq123d φ F C : C 1-1 onto D x C B : C 1-1 onto ran x C B
103 26 102 mpbird φ F C : C 1-1 onto D