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

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→ ( 𝐵 ∪ { 𝑌 } ) )