Metamath Proof Explorer

Theorem hashf1lem1

Description: Lemma for hashf1 . (Contributed by Mario Carneiro, 17-Apr-2015) (Proof shortened by AV, 14-Aug-2024)

Ref Expression
Hypotheses hashf1lem2.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
hashf1lem2.2 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
hashf1lem2.3 ⊢ ( 𝜑 → ¬ 𝑧 ∈ 𝐴 )
hashf1lem2.4 ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) )
hashf1lem1.5 ⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1→ 𝐵 )
Assertion hashf1lem1 ( 𝜑 → { 𝑓 ∣ ( ( 𝑓 ↾ 𝐴 ) = 𝐹 ∧ 𝑓 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) } ≈ ( 𝐵 ∖ ran 𝐹 ) )

Proof

Step Hyp Ref Expression
1 hashf1lem2.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 hashf1lem2.2 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
3 hashf1lem2.3 ⊢ ( 𝜑 → ¬ 𝑧 ∈ 𝐴 )
4 hashf1lem2.4 ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) )
5 hashf1lem1.5 ⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1→ 𝐵 )
6 f1setex ⊢ ( 𝐵 ∈ Fin → { 𝑓 ∣ 𝑓 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 } ∈ V )
7 2 6 syl ⊢ ( 𝜑 → { 𝑓 ∣ 𝑓 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 } ∈ V )
8 abanssr ⊢ { 𝑓 ∣ ( ( 𝑓 ↾ 𝐴 ) = 𝐹 ∧ 𝑓 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) } ⊆ { 𝑓 ∣ 𝑓 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 }
9 8 a1i ⊢ ( 𝜑 → { 𝑓 ∣ ( ( 𝑓 ↾ 𝐴 ) = 𝐹 ∧ 𝑓 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) } ⊆ { 𝑓 ∣ 𝑓 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 } )
10 7 9 ssexd ⊢ ( 𝜑 → { 𝑓 ∣ ( ( 𝑓 ↾ 𝐴 ) = 𝐹 ∧ 𝑓 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) } ∈ V )
11 2 difexd ⊢ ( 𝜑 → ( 𝐵 ∖ ran 𝐹 ) ∈ V )
12 vex ⊢ 𝑔 ∈ V
13 reseq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ↾ 𝐴 ) = ( 𝑔 ↾ 𝐴 ) )
14 13 eqeq1d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 ↾ 𝐴 ) = 𝐹 ↔ ( 𝑔 ↾ 𝐴 ) = 𝐹 ) )
15 f1eq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ↔ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) )
16 14 15 anbi12d ⊢ ( 𝑓 = 𝑔 → ( ( ( 𝑓 ↾ 𝐴 ) = 𝐹 ∧ 𝑓 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ↔ ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ) )
17 12 16 elab ⊢ ( 𝑔 ∈ { 𝑓 ∣ ( ( 𝑓 ↾ 𝐴 ) = 𝐹 ∧ 𝑓 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) } ↔ ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) )
18 f1f ⊢ ( 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 → 𝑔 : ( 𝐴 ∪ { 𝑧 } ) ⟶ 𝐵 )
19 18 ad2antll ⊢ ( ( 𝜑 ∧ ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ) → 𝑔 : ( 𝐴 ∪ { 𝑧 } ) ⟶ 𝐵 )
20 ssun2 ⊢ { 𝑧 } ⊆ ( 𝐴 ∪ { 𝑧 } )
21 vex ⊢ 𝑧 ∈ V
22 21 snss ⊢ ( 𝑧 ∈ ( 𝐴 ∪ { 𝑧 } ) ↔ { 𝑧 } ⊆ ( 𝐴 ∪ { 𝑧 } ) )
23 20 22 mpbir ⊢ 𝑧 ∈ ( 𝐴 ∪ { 𝑧 } )
24 ffvelrn ⊢ ( ( 𝑔 : ( 𝐴 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ 𝑧 ∈ ( 𝐴 ∪ { 𝑧 } ) ) → ( 𝑔 ‘ 𝑧 ) ∈ 𝐵 )
25 19 23 24 sylancl ⊢ ( ( 𝜑 ∧ ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ) → ( 𝑔 ‘ 𝑧 ) ∈ 𝐵 )
26 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ) → ¬ 𝑧 ∈ 𝐴 )
27 df-ima ⊢ ( 𝑔 “ 𝐴 ) = ran ( 𝑔 ↾ 𝐴 )
28 simprl ⊢ ( ( 𝜑 ∧ ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ) → ( 𝑔 ↾ 𝐴 ) = 𝐹 )
29 28 rneqd ⊢ ( ( 𝜑 ∧ ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ) → ran ( 𝑔 ↾ 𝐴 ) = ran 𝐹 )
30 27 29 syl5eq ⊢ ( ( 𝜑 ∧ ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ) → ( 𝑔 “ 𝐴 ) = ran 𝐹 )
31 30 eleq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ) → ( ( 𝑔 ‘ 𝑧 ) ∈ ( 𝑔 “ 𝐴 ) ↔ ( 𝑔 ‘ 𝑧 ) ∈ ran 𝐹 ) )
32 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ) → 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 )
33 23 a1i ⊢ ( ( 𝜑 ∧ ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ) → 𝑧 ∈ ( 𝐴 ∪ { 𝑧 } ) )
34 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ { 𝑧 } )
35 34 a1i ⊢ ( ( 𝜑 ∧ ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ) → 𝐴 ⊆ ( 𝐴 ∪ { 𝑧 } ) )
36 f1elima ⊢ ( ( 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ∧ 𝑧 ∈ ( 𝐴 ∪ { 𝑧 } ) ∧ 𝐴 ⊆ ( 𝐴 ∪ { 𝑧 } ) ) → ( ( 𝑔 ‘ 𝑧 ) ∈ ( 𝑔 “ 𝐴 ) ↔ 𝑧 ∈ 𝐴 ) )
37 32 33 35 36 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ) → ( ( 𝑔 ‘ 𝑧 ) ∈ ( 𝑔 “ 𝐴 ) ↔ 𝑧 ∈ 𝐴 ) )
38 31 37 bitr3d ⊢ ( ( 𝜑 ∧ ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ) → ( ( 𝑔 ‘ 𝑧 ) ∈ ran 𝐹 ↔ 𝑧 ∈ 𝐴 ) )
39 26 38 mtbird ⊢ ( ( 𝜑 ∧ ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ) → ¬ ( 𝑔 ‘ 𝑧 ) ∈ ran 𝐹 )
40 25 39 eldifd ⊢ ( ( 𝜑 ∧ ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ) → ( 𝑔 ‘ 𝑧 ) ∈ ( 𝐵 ∖ ran 𝐹 ) )
41 40 ex ⊢ ( 𝜑 → ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) → ( 𝑔 ‘ 𝑧 ) ∈ ( 𝐵 ∖ ran 𝐹 ) ) )
42 17 41 syl5bi ⊢ ( 𝜑 → ( 𝑔 ∈ { 𝑓 ∣ ( ( 𝑓 ↾ 𝐴 ) = 𝐹 ∧ 𝑓 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) } → ( 𝑔 ‘ 𝑧 ) ∈ ( 𝐵 ∖ ran 𝐹 ) ) )
43 f1f ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
44 5 43 syl ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
45 44 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
46 vex ⊢ 𝑥 ∈ V
47 21 46 f1osn ⊢ { ⟨ 𝑧 , 𝑥 ⟩ } : { 𝑧 } –1-1-onto→ { 𝑥 }
48 f1of ⊢ ( { ⟨ 𝑧 , 𝑥 ⟩ } : { 𝑧 } –1-1-onto→ { 𝑥 } → { ⟨ 𝑧 , 𝑥 ⟩ } : { 𝑧 } ⟶ { 𝑥 } )
49 47 48 ax-mp ⊢ { ⟨ 𝑧 , 𝑥 ⟩ } : { 𝑧 } ⟶ { 𝑥 }
50 eldifi ⊢ ( 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) → 𝑥 ∈ 𝐵 )
51 50 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → 𝑥 ∈ 𝐵 )
52 51 snssd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → { 𝑥 } ⊆ 𝐵 )
53 fss ⊢ ( ( { ⟨ 𝑧 , 𝑥 ⟩ } : { 𝑧 } ⟶ { 𝑥 } ∧ { 𝑥 } ⊆ 𝐵 ) → { ⟨ 𝑧 , 𝑥 ⟩ } : { 𝑧 } ⟶ 𝐵 )
54 49 52 53 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → { ⟨ 𝑧 , 𝑥 ⟩ } : { 𝑧 } ⟶ 𝐵 )
55 res0 ⊢ ( 𝐹 ↾ ∅ ) = ∅
56 res0 ⊢ ( { ⟨ 𝑧 , 𝑥 ⟩ } ↾ ∅ ) = ∅
57 55 56 eqtr4i ⊢ ( 𝐹 ↾ ∅ ) = ( { ⟨ 𝑧 , 𝑥 ⟩ } ↾ ∅ )
58 disjsn ⊢ ( ( 𝐴 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ 𝐴 )
59 3 58 sylibr ⊢ ( 𝜑 → ( 𝐴 ∩ { 𝑧 } ) = ∅ )
60 59 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → ( 𝐴 ∩ { 𝑧 } ) = ∅ )
61 60 reseq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → ( 𝐹 ↾ ( 𝐴 ∩ { 𝑧 } ) ) = ( 𝐹 ↾ ∅ ) )
62 60 reseq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → ( { ⟨ 𝑧 , 𝑥 ⟩ } ↾ ( 𝐴 ∩ { 𝑧 } ) ) = ( { ⟨ 𝑧 , 𝑥 ⟩ } ↾ ∅ ) )
63 57 61 62 3eqtr4a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → ( 𝐹 ↾ ( 𝐴 ∩ { 𝑧 } ) ) = ( { ⟨ 𝑧 , 𝑥 ⟩ } ↾ ( 𝐴 ∩ { 𝑧 } ) ) )
64 fresaunres1 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ { ⟨ 𝑧 , 𝑥 ⟩ } : { 𝑧 } ⟶ 𝐵 ∧ ( 𝐹 ↾ ( 𝐴 ∩ { 𝑧 } ) ) = ( { ⟨ 𝑧 , 𝑥 ⟩ } ↾ ( 𝐴 ∩ { 𝑧 } ) ) ) → ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ↾ 𝐴 ) = 𝐹 )
65 45 54 63 64 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ↾ 𝐴 ) = 𝐹 )
66 f1f1orn ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 )
67 5 66 syl ⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 )
68 67 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 )
69 47 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → { ⟨ 𝑧 , 𝑥 ⟩ } : { 𝑧 } –1-1-onto→ { 𝑥 } )
70 eldifn ⊢ ( 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) → ¬ 𝑥 ∈ ran 𝐹 )
71 70 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → ¬ 𝑥 ∈ ran 𝐹 )
72 disjsn ⊢ ( ( ran 𝐹 ∩ { 𝑥 } ) = ∅ ↔ ¬ 𝑥 ∈ ran 𝐹 )
73 71 72 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → ( ran 𝐹 ∩ { 𝑥 } ) = ∅ )
74 f1oun ⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 ∧ { ⟨ 𝑧 , 𝑥 ⟩ } : { 𝑧 } –1-1-onto→ { 𝑥 } ) ∧ ( ( 𝐴 ∩ { 𝑧 } ) = ∅ ∧ ( ran 𝐹 ∩ { 𝑥 } ) = ∅ ) ) → ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) : ( 𝐴 ∪ { 𝑧 } ) –1-1-onto→ ( ran 𝐹 ∪ { 𝑥 } ) )
75 68 69 60 73 74 syl22anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) : ( 𝐴 ∪ { 𝑧 } ) –1-1-onto→ ( ran 𝐹 ∪ { 𝑥 } ) )
76 f1of1 ⊢ ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) : ( 𝐴 ∪ { 𝑧 } ) –1-1-onto→ ( ran 𝐹 ∪ { 𝑥 } ) → ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) : ( 𝐴 ∪ { 𝑧 } ) –1-1→ ( ran 𝐹 ∪ { 𝑥 } ) )
77 75 76 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) : ( 𝐴 ∪ { 𝑧 } ) –1-1→ ( ran 𝐹 ∪ { 𝑥 } ) )
78 45 frnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → ran 𝐹 ⊆ 𝐵 )
79 78 52 unssd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → ( ran 𝐹 ∪ { 𝑥 } ) ⊆ 𝐵 )
80 f1ss ⊢ ( ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) : ( 𝐴 ∪ { 𝑧 } ) –1-1→ ( ran 𝐹 ∪ { 𝑥 } ) ∧ ( ran 𝐹 ∪ { 𝑥 } ) ⊆ 𝐵 ) → ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 )
81 77 79 80 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 )
82 44 1 fexd ⊢ ( 𝜑 → 𝐹 ∈ V )
83 82 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → 𝐹 ∈ V )
84 snex ⊢ { ⟨ 𝑧 , 𝑥 ⟩ } ∈ V
85 unexg ⊢ ( ( 𝐹 ∈ V ∧ { ⟨ 𝑧 , 𝑥 ⟩ } ∈ V ) → ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ∈ V )
86 83 84 85 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ∈ V )
87 reseq1 ⊢ ( 𝑓 = ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) → ( 𝑓 ↾ 𝐴 ) = ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ↾ 𝐴 ) )
88 87 eqeq1d ⊢ ( 𝑓 = ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) → ( ( 𝑓 ↾ 𝐴 ) = 𝐹 ↔ ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ↾ 𝐴 ) = 𝐹 ) )
89 f1eq1 ⊢ ( 𝑓 = ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) → ( 𝑓 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ↔ ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) )
90 88 89 anbi12d ⊢ ( 𝑓 = ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) → ( ( ( 𝑓 ↾ 𝐴 ) = 𝐹 ∧ 𝑓 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ↔ ( ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ↾ 𝐴 ) = 𝐹 ∧ ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ) )
91 90 elabg ⊢ ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ∈ V → ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ∈ { 𝑓 ∣ ( ( 𝑓 ↾ 𝐴 ) = 𝐹 ∧ 𝑓 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) } ↔ ( ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ↾ 𝐴 ) = 𝐹 ∧ ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ) )
92 86 91 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ∈ { 𝑓 ∣ ( ( 𝑓 ↾ 𝐴 ) = 𝐹 ∧ 𝑓 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) } ↔ ( ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ↾ 𝐴 ) = 𝐹 ∧ ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ) )
93 65 81 92 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ∈ { 𝑓 ∣ ( ( 𝑓 ↾ 𝐴 ) = 𝐹 ∧ 𝑓 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) } )
94 93 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) → ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ∈ { 𝑓 ∣ ( ( 𝑓 ↾ 𝐴 ) = 𝐹 ∧ 𝑓 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) } ) )
95 17 anbi1i ⊢ ( ( 𝑔 ∈ { 𝑓 ∣ ( ( 𝑓 ↾ 𝐴 ) = 𝐹 ∧ 𝑓 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) } ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ↔ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) )
96 simprlr ⊢ ( ( 𝜑 ∧ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ) → 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 )
97 f1fn ⊢ ( 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 → 𝑔 Fn ( 𝐴 ∪ { 𝑧 } ) )
98 96 97 syl ⊢ ( ( 𝜑 ∧ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ) → 𝑔 Fn ( 𝐴 ∪ { 𝑧 } ) )
99 75 adantrl ⊢ ( ( 𝜑 ∧ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ) → ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) : ( 𝐴 ∪ { 𝑧 } ) –1-1-onto→ ( ran 𝐹 ∪ { 𝑥 } ) )
100 f1ofn ⊢ ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) : ( 𝐴 ∪ { 𝑧 } ) –1-1-onto→ ( ran 𝐹 ∪ { 𝑥 } ) → ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) Fn ( 𝐴 ∪ { 𝑧 } ) )
101 99 100 syl ⊢ ( ( 𝜑 ∧ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ) → ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) Fn ( 𝐴 ∪ { 𝑧 } ) )
102 eqfnfv ⊢ ( ( 𝑔 Fn ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) Fn ( 𝐴 ∪ { 𝑧 } ) ) → ( 𝑔 = ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ↔ ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝑔 ‘ 𝑦 ) = ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ‘ 𝑦 ) ) )
103 98 101 102 syl2anc ⊢ ( ( 𝜑 ∧ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ) → ( 𝑔 = ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ↔ ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝑔 ‘ 𝑦 ) = ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ‘ 𝑦 ) ) )
104 fvres ⊢ ( 𝑦 ∈ 𝐴 → ( ( 𝑔 ↾ 𝐴 ) ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) )
105 104 eqcomd ⊢ ( 𝑦 ∈ 𝐴 → ( 𝑔 ‘ 𝑦 ) = ( ( 𝑔 ↾ 𝐴 ) ‘ 𝑦 ) )
106 simprll ⊢ ( ( 𝜑 ∧ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ) → ( 𝑔 ↾ 𝐴 ) = 𝐹 )
107 106 fveq1d ⊢ ( ( 𝜑 ∧ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ) → ( ( 𝑔 ↾ 𝐴 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
108 105 107 sylan9eqr ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
109 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝐹 : 𝐴 –1-1→ 𝐵 )
110 f1fn ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 Fn 𝐴 )
111 109 110 syl ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝐹 Fn 𝐴 )
112 21 46 fnsn ⊢ { ⟨ 𝑧 , 𝑥 ⟩ } Fn { 𝑧 }
113 112 a1i ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ) ∧ 𝑦 ∈ 𝐴 ) → { ⟨ 𝑧 , 𝑥 ⟩ } Fn { 𝑧 } )
114 59 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝐴 ∩ { 𝑧 } ) = ∅ )
115 simpr ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
116 111 113 114 115 fvun1d ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
117 108 116 eqtr4d ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑦 ) = ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ‘ 𝑦 ) )
118 117 ralrimiva ⊢ ( ( 𝜑 ∧ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ) → ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) = ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ‘ 𝑦 ) )
119 118 biantrurd ⊢ ( ( 𝜑 ∧ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ) → ( ∀ 𝑦 ∈ { 𝑧 } ( 𝑔 ‘ 𝑦 ) = ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ‘ 𝑦 ) ↔ ( ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) = ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ { 𝑧 } ( 𝑔 ‘ 𝑦 ) = ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ‘ 𝑦 ) ) ) )
120 ralunb ⊢ ( ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝑔 ‘ 𝑦 ) = ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ‘ 𝑦 ) ↔ ( ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) = ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ { 𝑧 } ( 𝑔 ‘ 𝑦 ) = ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ‘ 𝑦 ) ) )
121 119 120 bitr4di ⊢ ( ( 𝜑 ∧ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ) → ( ∀ 𝑦 ∈ { 𝑧 } ( 𝑔 ‘ 𝑦 ) = ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝑧 } ) ( 𝑔 ‘ 𝑦 ) = ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ‘ 𝑦 ) ) )
122 44 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
123 122 eleq2d ⊢ ( 𝜑 → ( 𝑧 ∈ dom 𝐹 ↔ 𝑧 ∈ 𝐴 ) )
124 3 123 mtbird ⊢ ( 𝜑 → ¬ 𝑧 ∈ dom 𝐹 )
125 124 adantr ⊢ ( ( 𝜑 ∧ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ) → ¬ 𝑧 ∈ dom 𝐹 )
126 fsnunfv ⊢ ( ( 𝑧 ∈ V ∧ 𝑥 ∈ V ∧ ¬ 𝑧 ∈ dom 𝐹 ) → ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ‘ 𝑧 ) = 𝑥 )
127 21 46 125 126 mp3an12i ⊢ ( ( 𝜑 ∧ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ) → ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ‘ 𝑧 ) = 𝑥 )
128 127 eqeq2d ⊢ ( ( 𝜑 ∧ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ) → ( ( 𝑔 ‘ 𝑧 ) = ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ‘ 𝑧 ) ↔ ( 𝑔 ‘ 𝑧 ) = 𝑥 ) )
129 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑔 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑧 ) )
130 fveq2 ⊢ ( 𝑦 = 𝑧 → ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ‘ 𝑦 ) = ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ‘ 𝑧 ) )
131 129 130 eqeq12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑔 ‘ 𝑦 ) = ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ‘ 𝑦 ) ↔ ( 𝑔 ‘ 𝑧 ) = ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ‘ 𝑧 ) ) )
132 21 131 ralsn ⊢ ( ∀ 𝑦 ∈ { 𝑧 } ( 𝑔 ‘ 𝑦 ) = ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ‘ 𝑦 ) ↔ ( 𝑔 ‘ 𝑧 ) = ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ‘ 𝑧 ) )
133 eqcom ⊢ ( 𝑥 = ( 𝑔 ‘ 𝑧 ) ↔ ( 𝑔 ‘ 𝑧 ) = 𝑥 )
134 128 132 133 3bitr4g ⊢ ( ( 𝜑 ∧ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ) → ( ∀ 𝑦 ∈ { 𝑧 } ( 𝑔 ‘ 𝑦 ) = ( ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ‘ 𝑦 ) ↔ 𝑥 = ( 𝑔 ‘ 𝑧 ) ) )
135 103 121 134 3bitr2d ⊢ ( ( 𝜑 ∧ ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) ) → ( 𝑔 = ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ↔ 𝑥 = ( 𝑔 ‘ 𝑧 ) ) )
136 135 ex ⊢ ( 𝜑 → ( ( ( ( 𝑔 ↾ 𝐴 ) = 𝐹 ∧ 𝑔 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → ( 𝑔 = ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ↔ 𝑥 = ( 𝑔 ‘ 𝑧 ) ) ) )
137 95 136 syl5bi ⊢ ( 𝜑 → ( ( 𝑔 ∈ { 𝑓 ∣ ( ( 𝑓 ↾ 𝐴 ) = 𝐹 ∧ 𝑓 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) } ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝐹 ) ) → ( 𝑔 = ( 𝐹 ∪ { ⟨ 𝑧 , 𝑥 ⟩ } ) ↔ 𝑥 = ( 𝑔 ‘ 𝑧 ) ) ) )
138 10 11 42 94 137 en3d ⊢ ( 𝜑 → { 𝑓 ∣ ( ( 𝑓 ↾ 𝐴 ) = 𝐹 ∧ 𝑓 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 ) } ≈ ( 𝐵 ∖ ran 𝐹 ) )