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
|- F = ( G u. { <. X , Y >. } )
Assertion f1ounsn
|- ( ( G : A -1-1-onto-> B /\ ( X e. V /\ Y e. W ) /\ ( X e/ A /\ Y e/ B ) ) -> F : ( A u. { X } ) -1-1-onto-> ( B u. { Y } ) )

Proof

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