This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 sselid ⊢ ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐴 )
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→ 𝐷 )