Metamath Proof Explorer


Theorem f1ounsn

Description: Extension of a bijection by an ordered pair. (Contributed by AV, 15-Sep-2025)

Ref Expression
Hypothesis f1ounsn.f 𝐹 = ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } )
Assertion f1ounsn ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → 𝐹 : ( 𝐴 ∪ { 𝑋 } ) –1-1-onto→ ( 𝐵 ∪ { 𝑌 } ) )

Proof

Step Hyp Ref Expression
1 f1ounsn.f 𝐹 = ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } )
2 f1of ( 𝐺 : 𝐴1-1-onto𝐵𝐺 : 𝐴𝐵 )
3 ssun1 𝐵 ⊆ ( 𝐵 ∪ { 𝑌 } )
4 3 a1i ( 𝐺 : 𝐴1-1-onto𝐵𝐵 ⊆ ( 𝐵 ∪ { 𝑌 } ) )
5 2 4 fssd ( 𝐺 : 𝐴1-1-onto𝐵𝐺 : 𝐴 ⟶ ( 𝐵 ∪ { 𝑌 } ) )
6 5 3ad2ant1 ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → 𝐺 : 𝐴 ⟶ ( 𝐵 ∪ { 𝑌 } ) )
7 simpl ( ( 𝑋𝑉𝑌𝑊 ) → 𝑋𝑉 )
8 df-nel ( 𝑋𝐴 ↔ ¬ 𝑋𝐴 )
9 8 biimpi ( 𝑋𝐴 → ¬ 𝑋𝐴 )
10 9 adantr ( ( 𝑋𝐴𝑌𝐵 ) → ¬ 𝑋𝐴 )
11 7 10 anim12i ( ( ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ( 𝑋𝑉 ∧ ¬ 𝑋𝐴 ) )
12 11 3adant1 ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ( 𝑋𝑉 ∧ ¬ 𝑋𝐴 ) )
13 eqid 𝑌 = 𝑌
14 13 olci ( 𝑌𝐵𝑌 = 𝑌 )
15 elunsn ( 𝑌𝑊 → ( 𝑌 ∈ ( 𝐵 ∪ { 𝑌 } ) ↔ ( 𝑌𝐵𝑌 = 𝑌 ) ) )
16 14 15 mpbiri ( 𝑌𝑊𝑌 ∈ ( 𝐵 ∪ { 𝑌 } ) )
17 16 adantl ( ( 𝑋𝑉𝑌𝑊 ) → 𝑌 ∈ ( 𝐵 ∪ { 𝑌 } ) )
18 17 3ad2ant2 ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → 𝑌 ∈ ( 𝐵 ∪ { 𝑌 } ) )
19 6 12 18 3jca ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ( 𝐺 : 𝐴 ⟶ ( 𝐵 ∪ { 𝑌 } ) ∧ ( 𝑋𝑉 ∧ ¬ 𝑋𝐴 ) ∧ 𝑌 ∈ ( 𝐵 ∪ { 𝑌 } ) ) )
20 fsnunf ( ( 𝐺 : 𝐴 ⟶ ( 𝐵 ∪ { 𝑌 } ) ∧ ( 𝑋𝑉 ∧ ¬ 𝑋𝐴 ) ∧ 𝑌 ∈ ( 𝐵 ∪ { 𝑌 } ) ) → ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : ( 𝐴 ∪ { 𝑋 } ) ⟶ ( 𝐵 ∪ { 𝑌 } ) )
21 19 20 syl ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : ( 𝐴 ∪ { 𝑋 } ) ⟶ ( 𝐵 ∪ { 𝑌 } ) )
22 f1of1 ( 𝐺 : 𝐴1-1-onto𝐵𝐺 : 𝐴1-1𝐵 )
23 dff14a ( 𝐺 : 𝐴1-1𝐵 ↔ ( 𝐺 : 𝐴𝐵 ∧ ∀ 𝑎𝐴𝑏𝐴 ( 𝑎𝑏 → ( 𝐺𝑎 ) ≠ ( 𝐺𝑏 ) ) ) )
24 neeq1 ( 𝑎 = 𝑥 → ( 𝑎𝑏𝑥𝑏 ) )
25 fveq2 ( 𝑎 = 𝑥 → ( 𝐺𝑎 ) = ( 𝐺𝑥 ) )
26 25 neeq1d ( 𝑎 = 𝑥 → ( ( 𝐺𝑎 ) ≠ ( 𝐺𝑏 ) ↔ ( 𝐺𝑥 ) ≠ ( 𝐺𝑏 ) ) )
27 24 26 imbi12d ( 𝑎 = 𝑥 → ( ( 𝑎𝑏 → ( 𝐺𝑎 ) ≠ ( 𝐺𝑏 ) ) ↔ ( 𝑥𝑏 → ( 𝐺𝑥 ) ≠ ( 𝐺𝑏 ) ) ) )
28 neeq2 ( 𝑏 = 𝑦 → ( 𝑥𝑏𝑥𝑦 ) )
29 fveq2 ( 𝑏 = 𝑦 → ( 𝐺𝑏 ) = ( 𝐺𝑦 ) )
30 29 neeq2d ( 𝑏 = 𝑦 → ( ( 𝐺𝑥 ) ≠ ( 𝐺𝑏 ) ↔ ( 𝐺𝑥 ) ≠ ( 𝐺𝑦 ) ) )
31 28 30 imbi12d ( 𝑏 = 𝑦 → ( ( 𝑥𝑏 → ( 𝐺𝑥 ) ≠ ( 𝐺𝑏 ) ) ↔ ( 𝑥𝑦 → ( 𝐺𝑥 ) ≠ ( 𝐺𝑦 ) ) ) )
32 27 31 rspc2va ( ( ( 𝑥𝐴𝑦𝐴 ) ∧ ∀ 𝑎𝐴𝑏𝐴 ( 𝑎𝑏 → ( 𝐺𝑎 ) ≠ ( 𝐺𝑏 ) ) ) → ( 𝑥𝑦 → ( 𝐺𝑥 ) ≠ ( 𝐺𝑦 ) ) )
33 32 expcom ( ∀ 𝑎𝐴𝑏𝐴 ( 𝑎𝑏 → ( 𝐺𝑎 ) ≠ ( 𝐺𝑏 ) ) → ( ( 𝑥𝐴𝑦𝐴 ) → ( 𝑥𝑦 → ( 𝐺𝑥 ) ≠ ( 𝐺𝑦 ) ) ) )
34 33 adantl ( ( 𝐺 : 𝐴𝐵 ∧ ∀ 𝑎𝐴𝑏𝐴 ( 𝑎𝑏 → ( 𝐺𝑎 ) ≠ ( 𝐺𝑏 ) ) ) → ( ( 𝑥𝐴𝑦𝐴 ) → ( 𝑥𝑦 → ( 𝐺𝑥 ) ≠ ( 𝐺𝑦 ) ) ) )
35 23 34 sylbi ( 𝐺 : 𝐴1-1𝐵 → ( ( 𝑥𝐴𝑦𝐴 ) → ( 𝑥𝑦 → ( 𝐺𝑥 ) ≠ ( 𝐺𝑦 ) ) ) )
36 22 35 syl ( 𝐺 : 𝐴1-1-onto𝐵 → ( ( 𝑥𝐴𝑦𝐴 ) → ( 𝑥𝑦 → ( 𝐺𝑥 ) ≠ ( 𝐺𝑦 ) ) ) )
37 36 3ad2ant1 ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ( ( 𝑥𝐴𝑦𝐴 ) → ( 𝑥𝑦 → ( 𝐺𝑥 ) ≠ ( 𝐺𝑦 ) ) ) )
38 37 impl ( ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) ∧ 𝑦𝐴 ) → ( 𝑥𝑦 → ( 𝐺𝑥 ) ≠ ( 𝐺𝑦 ) ) )
39 38 imp ( ( ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) ∧ 𝑦𝐴 ) ∧ 𝑥𝑦 ) → ( 𝐺𝑥 ) ≠ ( 𝐺𝑦 ) )
40 nelne2 ( ( 𝑥𝐴 ∧ ¬ 𝑋𝐴 ) → 𝑥𝑋 )
41 40 necomd ( ( 𝑥𝐴 ∧ ¬ 𝑋𝐴 ) → 𝑋𝑥 )
42 41 expcom ( ¬ 𝑋𝐴 → ( 𝑥𝐴𝑋𝑥 ) )
43 8 42 sylbi ( 𝑋𝐴 → ( 𝑥𝐴𝑋𝑥 ) )
44 43 adantr ( ( 𝑋𝐴𝑌𝐵 ) → ( 𝑥𝐴𝑋𝑥 ) )
45 44 3ad2ant3 ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ( 𝑥𝐴𝑋𝑥 ) )
46 45 imp ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) → 𝑋𝑥 )
47 46 adantr ( ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) ∧ 𝑦𝐴 ) → 𝑋𝑥 )
48 47 adantr ( ( ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) ∧ 𝑦𝐴 ) ∧ 𝑥𝑦 ) → 𝑋𝑥 )
49 fvunsn ( 𝑋𝑥 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) = ( 𝐺𝑥 ) )
50 48 49 syl ( ( ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) ∧ 𝑦𝐴 ) ∧ 𝑥𝑦 ) → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) = ( 𝐺𝑥 ) )
51 nelne2 ( ( 𝑦𝐴 ∧ ¬ 𝑋𝐴 ) → 𝑦𝑋 )
52 51 necomd ( ( 𝑦𝐴 ∧ ¬ 𝑋𝐴 ) → 𝑋𝑦 )
53 52 expcom ( ¬ 𝑋𝐴 → ( 𝑦𝐴𝑋𝑦 ) )
54 8 53 sylbi ( 𝑋𝐴 → ( 𝑦𝐴𝑋𝑦 ) )
55 54 adantr ( ( 𝑋𝐴𝑌𝐵 ) → ( 𝑦𝐴𝑋𝑦 ) )
56 55 3ad2ant3 ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ( 𝑦𝐴𝑋𝑦 ) )
57 56 adantr ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) → ( 𝑦𝐴𝑋𝑦 ) )
58 57 imp ( ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) ∧ 𝑦𝐴 ) → 𝑋𝑦 )
59 58 adantr ( ( ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) ∧ 𝑦𝐴 ) ∧ 𝑥𝑦 ) → 𝑋𝑦 )
60 fvunsn ( 𝑋𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) = ( 𝐺𝑦 ) )
61 59 60 syl ( ( ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) ∧ 𝑦𝐴 ) ∧ 𝑥𝑦 ) → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) = ( 𝐺𝑦 ) )
62 39 50 61 3netr4d ( ( ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) ∧ 𝑦𝐴 ) ∧ 𝑥𝑦 ) → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) )
63 62 ex ( ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) ∧ 𝑦𝐴 ) → ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) )
64 63 ralrimiva ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) → ∀ 𝑦𝐴 ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) )
65 2 3ad2ant1 ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → 𝐺 : 𝐴𝐵 )
66 65 ffvelcdmda ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) → ( 𝐺𝑥 ) ∈ 𝐵 )
67 df-nel ( 𝑌𝐵 ↔ ¬ 𝑌𝐵 )
68 67 biimpi ( 𝑌𝐵 → ¬ 𝑌𝐵 )
69 68 adantl ( ( 𝑋𝐴𝑌𝐵 ) → ¬ 𝑌𝐵 )
70 69 3ad2ant3 ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ¬ 𝑌𝐵 )
71 70 adantr ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) → ¬ 𝑌𝐵 )
72 nelne2 ( ( ( 𝐺𝑥 ) ∈ 𝐵 ∧ ¬ 𝑌𝐵 ) → ( 𝐺𝑥 ) ≠ 𝑌 )
73 66 71 72 syl2anc ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) → ( 𝐺𝑥 ) ≠ 𝑌 )
74 73 adantr ( ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) ∧ 𝑥𝑋 ) → ( 𝐺𝑥 ) ≠ 𝑌 )
75 simpr ( ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) ∧ 𝑥𝑋 ) → 𝑥𝑋 )
76 75 necomd ( ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) ∧ 𝑥𝑋 ) → 𝑋𝑥 )
77 76 49 syl ( ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) ∧ 𝑥𝑋 ) → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) = ( 𝐺𝑥 ) )
78 7 3ad2ant2 ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → 𝑋𝑉 )
79 simpr ( ( 𝑋𝑉𝑌𝑊 ) → 𝑌𝑊 )
80 79 3ad2ant2 ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → 𝑌𝑊 )
81 f1odm ( 𝐺 : 𝐴1-1-onto𝐵 → dom 𝐺 = 𝐴 )
82 81 eqcomd ( 𝐺 : 𝐴1-1-onto𝐵𝐴 = dom 𝐺 )
83 82 eleq2d ( 𝐺 : 𝐴1-1-onto𝐵 → ( 𝑋𝐴𝑋 ∈ dom 𝐺 ) )
84 83 notbid ( 𝐺 : 𝐴1-1-onto𝐵 → ( ¬ 𝑋𝐴 ↔ ¬ 𝑋 ∈ dom 𝐺 ) )
85 8 84 bitrid ( 𝐺 : 𝐴1-1-onto𝐵 → ( 𝑋𝐴 ↔ ¬ 𝑋 ∈ dom 𝐺 ) )
86 85 biimpd ( 𝐺 : 𝐴1-1-onto𝐵 → ( 𝑋𝐴 → ¬ 𝑋 ∈ dom 𝐺 ) )
87 86 adantrd ( 𝐺 : 𝐴1-1-onto𝐵 → ( ( 𝑋𝐴𝑌𝐵 ) → ¬ 𝑋 ∈ dom 𝐺 ) )
88 87 imp ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ¬ 𝑋 ∈ dom 𝐺 )
89 88 3adant2 ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ¬ 𝑋 ∈ dom 𝐺 )
90 78 80 89 3jca ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ( 𝑋𝑉𝑌𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺 ) )
91 90 adantr ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) → ( 𝑋𝑉𝑌𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺 ) )
92 91 adantr ( ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) ∧ 𝑥𝑋 ) → ( 𝑋𝑉𝑌𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺 ) )
93 fsnunfv ( ( 𝑋𝑉𝑌𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺 ) → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) = 𝑌 )
94 92 93 syl ( ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) ∧ 𝑥𝑋 ) → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) = 𝑌 )
95 74 77 94 3netr4d ( ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) ∧ 𝑥𝑋 ) → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) )
96 95 ex ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) → ( 𝑥𝑋 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ) )
97 78 adantr ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) → 𝑋𝑉 )
98 neeq2 ( 𝑦 = 𝑋 → ( 𝑥𝑦𝑥𝑋 ) )
99 fveq2 ( 𝑦 = 𝑋 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) = ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) )
100 99 neeq2d ( 𝑦 = 𝑋 → ( ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ↔ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ) )
101 98 100 imbi12d ( 𝑦 = 𝑋 → ( ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ↔ ( 𝑥𝑋 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ) ) )
102 101 ralsng ( 𝑋𝑉 → ( ∀ 𝑦 ∈ { 𝑋 } ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ↔ ( 𝑥𝑋 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ) ) )
103 97 102 syl ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) → ( ∀ 𝑦 ∈ { 𝑋 } ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ↔ ( 𝑥𝑋 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ) ) )
104 96 103 mpbird ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) → ∀ 𝑦 ∈ { 𝑋 } ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) )
105 ralun ( ( ∀ 𝑦𝐴 ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ { 𝑋 } ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ) → ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝑋 } ) ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) )
106 64 104 105 syl2anc ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑥𝐴 ) → ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝑋 } ) ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) )
107 106 ralrimiva ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ∀ 𝑥𝐴𝑦 ∈ ( 𝐴 ∪ { 𝑋 } ) ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) )
108 65 ffvelcdmda ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑦𝐴 ) → ( 𝐺𝑦 ) ∈ 𝐵 )
109 70 adantr ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑦𝐴 ) → ¬ 𝑌𝐵 )
110 108 109 jca ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑦𝐴 ) → ( ( 𝐺𝑦 ) ∈ 𝐵 ∧ ¬ 𝑌𝐵 ) )
111 110 adantr ( ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑦𝐴 ) ∧ 𝑋𝑦 ) → ( ( 𝐺𝑦 ) ∈ 𝐵 ∧ ¬ 𝑌𝐵 ) )
112 nelne2 ( ( ( 𝐺𝑦 ) ∈ 𝐵 ∧ ¬ 𝑌𝐵 ) → ( 𝐺𝑦 ) ≠ 𝑌 )
113 112 necomd ( ( ( 𝐺𝑦 ) ∈ 𝐵 ∧ ¬ 𝑌𝐵 ) → 𝑌 ≠ ( 𝐺𝑦 ) )
114 111 113 syl ( ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑦𝐴 ) ∧ 𝑋𝑦 ) → 𝑌 ≠ ( 𝐺𝑦 ) )
115 90 adantr ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑦𝐴 ) → ( 𝑋𝑉𝑌𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺 ) )
116 115 adantr ( ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑦𝐴 ) ∧ 𝑋𝑦 ) → ( 𝑋𝑉𝑌𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺 ) )
117 116 93 syl ( ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑦𝐴 ) ∧ 𝑋𝑦 ) → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) = 𝑌 )
118 60 adantl ( ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑦𝐴 ) ∧ 𝑋𝑦 ) → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) = ( 𝐺𝑦 ) )
119 114 117 118 3netr4d ( ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑦𝐴 ) ∧ 𝑋𝑦 ) → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) )
120 119 ex ( ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) ∧ 𝑦𝐴 ) → ( 𝑋𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) )
121 120 ralrimiva ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ∀ 𝑦𝐴 ( 𝑋𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) )
122 eqid 𝑋 = 𝑋
123 eqneqall ( 𝑋 = 𝑋 → ( 𝑋𝑋 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ) )
124 122 123 ax-mp ( 𝑋𝑋 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) )
125 neeq2 ( 𝑦 = 𝑋 → ( 𝑋𝑦𝑋𝑋 ) )
126 99 neeq2d ( 𝑦 = 𝑋 → ( ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ↔ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ) )
127 125 126 imbi12d ( 𝑦 = 𝑋 → ( ( 𝑋𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ↔ ( 𝑋𝑋 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ) ) )
128 127 ralsng ( 𝑋𝑉 → ( ∀ 𝑦 ∈ { 𝑋 } ( 𝑋𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ↔ ( 𝑋𝑋 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ) ) )
129 78 128 syl ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ( ∀ 𝑦 ∈ { 𝑋 } ( 𝑋𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ↔ ( 𝑋𝑋 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ) ) )
130 124 129 mpbiri ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ∀ 𝑦 ∈ { 𝑋 } ( 𝑋𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) )
131 ralun ( ( ∀ 𝑦𝐴 ( 𝑋𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ { 𝑋 } ( 𝑋𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ) → ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝑋 } ) ( 𝑋𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) )
132 121 130 131 syl2anc ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝑋 } ) ( 𝑋𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) )
133 neeq1 ( 𝑥 = 𝑋 → ( 𝑥𝑦𝑋𝑦 ) )
134 fveq2 ( 𝑥 = 𝑋 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) = ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) )
135 134 neeq1d ( 𝑥 = 𝑋 → ( ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ↔ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) )
136 133 135 imbi12d ( 𝑥 = 𝑋 → ( ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ↔ ( 𝑋𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ) )
137 136 ralbidv ( 𝑥 = 𝑋 → ( ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝑋 } ) ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝑋 } ) ( 𝑋𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ) )
138 137 ralsng ( 𝑋𝑉 → ( ∀ 𝑥 ∈ { 𝑋 } ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝑋 } ) ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝑋 } ) ( 𝑋𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ) )
139 78 138 syl ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ( ∀ 𝑥 ∈ { 𝑋 } ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝑋 } ) ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝑋 } ) ( 𝑋𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ) )
140 132 139 mpbird ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ∀ 𝑥 ∈ { 𝑋 } ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝑋 } ) ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) )
141 ralun ( ( ∀ 𝑥𝐴𝑦 ∈ ( 𝐴 ∪ { 𝑋 } ) ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ∧ ∀ 𝑥 ∈ { 𝑋 } ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝑋 } ) ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ) → ∀ 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝑋 } ) ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) )
142 107 140 141 syl2anc ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ∀ 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝑋 } ) ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) )
143 21 142 jca ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : ( 𝐴 ∪ { 𝑋 } ) ⟶ ( 𝐵 ∪ { 𝑌 } ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝑋 } ) ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ) )
144 rnun ran ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) = ( ran 𝐺 ∪ ran { ⟨ 𝑋 , 𝑌 ⟩ } )
145 f1ofo ( 𝐺 : 𝐴1-1-onto𝐵𝐺 : 𝐴onto𝐵 )
146 forn ( 𝐺 : 𝐴onto𝐵 → ran 𝐺 = 𝐵 )
147 145 146 syl ( 𝐺 : 𝐴1-1-onto𝐵 → ran 𝐺 = 𝐵 )
148 147 3ad2ant1 ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ran 𝐺 = 𝐵 )
149 rnsnopg ( 𝑋𝑉 → ran { ⟨ 𝑋 , 𝑌 ⟩ } = { 𝑌 } )
150 149 adantr ( ( 𝑋𝑉𝑌𝑊 ) → ran { ⟨ 𝑋 , 𝑌 ⟩ } = { 𝑌 } )
151 150 3ad2ant2 ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ran { ⟨ 𝑋 , 𝑌 ⟩ } = { 𝑌 } )
152 148 151 uneq12d ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ( ran 𝐺 ∪ ran { ⟨ 𝑋 , 𝑌 ⟩ } ) = ( 𝐵 ∪ { 𝑌 } ) )
153 144 152 eqtrid ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ran ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) = ( 𝐵 ∪ { 𝑌 } ) )
154 143 153 jca ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ( ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : ( 𝐴 ∪ { 𝑋 } ) ⟶ ( 𝐵 ∪ { 𝑌 } ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝑋 } ) ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ) ∧ ran ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) = ( 𝐵 ∪ { 𝑌 } ) ) )
155 dff1o5 ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : ( 𝐴 ∪ { 𝑋 } ) –1-1-onto→ ( 𝐵 ∪ { 𝑌 } ) ↔ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : ( 𝐴 ∪ { 𝑋 } ) –1-1→ ( 𝐵 ∪ { 𝑌 } ) ∧ ran ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) = ( 𝐵 ∪ { 𝑌 } ) ) )
156 dff14a ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : ( 𝐴 ∪ { 𝑋 } ) –1-1→ ( 𝐵 ∪ { 𝑌 } ) ↔ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : ( 𝐴 ∪ { 𝑋 } ) ⟶ ( 𝐵 ∪ { 𝑌 } ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝑋 } ) ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ) )
157 155 156 bianbi ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : ( 𝐴 ∪ { 𝑋 } ) –1-1-onto→ ( 𝐵 ∪ { 𝑌 } ) ↔ ( ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : ( 𝐴 ∪ { 𝑋 } ) ⟶ ( 𝐵 ∪ { 𝑌 } ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝑋 } ) ( 𝑥𝑦 → ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑥 ) ≠ ( ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑦 ) ) ) ∧ ran ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) = ( 𝐵 ∪ { 𝑌 } ) ) )
158 154 157 sylibr ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : ( 𝐴 ∪ { 𝑋 } ) –1-1-onto→ ( 𝐵 ∪ { 𝑌 } ) )
159 f1oeq1 ( 𝐹 = ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) → ( 𝐹 : ( 𝐴 ∪ { 𝑋 } ) –1-1-onto→ ( 𝐵 ∪ { 𝑌 } ) ↔ ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : ( 𝐴 ∪ { 𝑋 } ) –1-1-onto→ ( 𝐵 ∪ { 𝑌 } ) ) )
160 1 159 ax-mp ( 𝐹 : ( 𝐴 ∪ { 𝑋 } ) –1-1-onto→ ( 𝐵 ∪ { 𝑌 } ) ↔ ( 𝐺 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : ( 𝐴 ∪ { 𝑋 } ) –1-1-onto→ ( 𝐵 ∪ { 𝑌 } ) )
161 158 160 sylibr ( ( 𝐺 : 𝐴1-1-onto𝐵 ∧ ( 𝑋𝑉𝑌𝑊 ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → 𝐹 : ( 𝐴 ∪ { 𝑋 } ) –1-1-onto→ ( 𝐵 ∪ { 𝑌 } ) )