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 
|- 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 } ) )