f1ounsn

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

		Ref	Expression
	Hypothesis	f1ounsn.f	$⊢ F = G \cup \{⟨X, Y⟩\}$
	Assertion	f1ounsn	$⊢ (G : A \underset{1-1 onto}{⟶} B \land (X \in V \land Y \in W) \land (X \notin A \land Y \notin B)) \to F : A \cup \{X\} \underset{1-1 onto}{⟶} B \cup \{Y\}$

Proof

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

Metamath Proof Explorer

Theorem f1ounsn

Proof