Metamath Proof Explorer

Theorem hashf1lem1

Description: Lemma for hashf1 . (Contributed by Mario Carneiro, 17-Apr-2015)

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