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 X Y
Assertion f1ounsn G : A 1-1 onto B X V Y W X A Y B F : A X 1-1 onto B Y

Proof

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