Metamath Proof Explorer


Theorem disjf1o

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

Ref Expression
Hypotheses disjf1o.xph 𝑥 𝜑
disjf1o.f 𝐹 = ( 𝑥𝐴𝐵 )
disjf1o.b ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
disjf1o.dj ( 𝜑Disj 𝑥𝐴 𝐵 )
disjf1o.d 𝐶 = { 𝑥𝐴𝐵 ≠ ∅ }
disjf1o.e 𝐷 = ( ran 𝐹 ∖ { ∅ } )
Assertion disjf1o ( 𝜑 → ( 𝐹𝐶 ) : 𝐶1-1-onto𝐷 )

Proof

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