f1ounsn - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > f1ounsn		Structured version Visualization version GIF version

Theorem f1ounsn 7291

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

**Hypothesis**
Ref	Expression
f1ounsn.f	⊢ 𝐹 = (𝐺 ∪ {⟨𝑋, 𝑌⟩})

**Assertion**
Ref	Expression
f1ounsn	⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝐹:(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}))

Proof of Theorem f1ounsn Dummy variables 𝑎 𝑏 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		f1of 6848	. . . . . . . . 9 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐺:𝐴⟶𝐵)
2		ssun1 4187	. . . . . . . . . 10 ⊢ 𝐵 ⊆ (𝐵 ∪ {𝑌})
3	2	a1i 11	. . . . . . . . 9 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐵 ⊆ (𝐵 ∪ {𝑌}))
4	1, 3	fssd 6753	. . . . . . . 8 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐺:𝐴⟶(𝐵 ∪ {𝑌}))
5	4	3ad2ant1 1132	. . . . . . 7 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝐺:𝐴⟶(𝐵 ∪ {𝑌}))
6		simpl 482	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → 𝑋 ∈ 𝑉)
7		df-nel 3044	. . . . . . . . . . 11 ⊢ (𝑋 ∉ 𝐴 ↔ ¬ 𝑋 ∈ 𝐴)
8	7	biimpi 216	. . . . . . . . . 10 ⊢ (𝑋 ∉ 𝐴 → ¬ 𝑋 ∈ 𝐴)
9	8	adantr 480	. . . . . . . . 9 ⊢ ((𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵) → ¬ 𝑋 ∈ 𝐴)
10	6, 9	anim12i 613	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝐴))
11	10	3adant1 1129	. . . . . . 7 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝐴))
12		eqid 2734	. . . . . . . . . . 11 ⊢ 𝑌 = 𝑌
13	12	olci 866	. . . . . . . . . 10 ⊢ (𝑌 ∈ 𝐵 ∨ 𝑌 = 𝑌)
14		elunsn 4687	. . . . . . . . . 10 ⊢ (𝑌 ∈ 𝑊 → (𝑌 ∈ (𝐵 ∪ {𝑌}) ↔ (𝑌 ∈ 𝐵 ∨ 𝑌 = 𝑌)))
15	13, 14	mpbiri 258	. . . . . . . . 9 ⊢ (𝑌 ∈ 𝑊 → 𝑌 ∈ (𝐵 ∪ {𝑌}))
16	15	adantl 481	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → 𝑌 ∈ (𝐵 ∪ {𝑌}))
17	16	3ad2ant2 1133	. . . . . . 7 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝑌 ∈ (𝐵 ∪ {𝑌}))
18	5, 11, 17	3jca 1127	. . . . . 6 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝐺:𝐴⟶(𝐵 ∪ {𝑌}) ∧ (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝐴) ∧ 𝑌 ∈ (𝐵 ∪ {𝑌})))
19		fsnunf 7204	. . . . . 6 ⊢ ((𝐺:𝐴⟶(𝐵 ∪ {𝑌}) ∧ (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝐴) ∧ 𝑌 ∈ (𝐵 ∪ {𝑌})) → (𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}))
20	18, 19	syl 17	. . . . 5 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}))
21		f1of1 6847	. . . . . . . . . . . . . . 15 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐺:𝐴–1-1→𝐵)
22		dff14a 7289	. . . . . . . . . . . . . . . 16 ⊢ (𝐺:𝐴–1-1→𝐵 ↔ (𝐺:𝐴⟶𝐵 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎 ≠ 𝑏 → (𝐺‘𝑎) ≠ (𝐺‘𝑏))))
23		neeq1 3000	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑥 → (𝑎 ≠ 𝑏 ↔ 𝑥 ≠ 𝑏))
24		fveq2 6906	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑥 → (𝐺‘𝑎) = (𝐺‘𝑥))
25	24	neeq1d 2997	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑥 → ((𝐺‘𝑎) ≠ (𝐺‘𝑏) ↔ (𝐺‘𝑥) ≠ (𝐺‘𝑏)))
26	23, 25	imbi12d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑥 → ((𝑎 ≠ 𝑏 → (𝐺‘𝑎) ≠ (𝐺‘𝑏)) ↔ (𝑥 ≠ 𝑏 → (𝐺‘𝑥) ≠ (𝐺‘𝑏))))
27		neeq2 3001	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = 𝑦 → (𝑥 ≠ 𝑏 ↔ 𝑥 ≠ 𝑦))
28		fveq2 6906	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = 𝑦 → (𝐺‘𝑏) = (𝐺‘𝑦))
29	28	neeq2d 2998	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = 𝑦 → ((𝐺‘𝑥) ≠ (𝐺‘𝑏) ↔ (𝐺‘𝑥) ≠ (𝐺‘𝑦)))
30	27, 29	imbi12d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 𝑦 → ((𝑥 ≠ 𝑏 → (𝐺‘𝑥) ≠ (𝐺‘𝑏)) ↔ (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
31	26, 30	rspc2va 3633	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎 ≠ 𝑏 → (𝐺‘𝑎) ≠ (𝐺‘𝑏))) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)))
32	31	expcom 413	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎 ≠ 𝑏 → (𝐺‘𝑎) ≠ (𝐺‘𝑏)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
33	32	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺:𝐴⟶𝐵 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎 ≠ 𝑏 → (𝐺‘𝑎) ≠ (𝐺‘𝑏))) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
34	22, 33	sylbi 217	. . . . . . . . . . . . . . 15 ⊢ (𝐺:𝐴–1-1→𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
35	21, 34	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
36	35	3ad2ant1 1132	. . . . . . . . . . . . 13 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
37	36	impl 455	. . . . . . . . . . . 12 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)))
38	37	imp 406	. . . . . . . . . . 11 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → (𝐺‘𝑥) ≠ (𝐺‘𝑦))
39		nelne2 3037	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑥 ≠ 𝑋)
40	39	necomd 2993	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑋 ≠ 𝑥)
41	40	expcom 413	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑋 ∈ 𝐴 → (𝑥 ∈ 𝐴 → 𝑋 ≠ 𝑥))
42	7, 41	sylbi 217	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∉ 𝐴 → (𝑥 ∈ 𝐴 → 𝑋 ≠ 𝑥))
43	42	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵) → (𝑥 ∈ 𝐴 → 𝑋 ≠ 𝑥))
44	43	3ad2ant3 1134	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝑥 ∈ 𝐴 → 𝑋 ≠ 𝑥))
45	44	imp 406	. . . . . . . . . . . . . 14 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑋 ≠ 𝑥)
46	45	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑋 ≠ 𝑥)
47	46	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → 𝑋 ≠ 𝑥)
48		fvunsn 7198	. . . . . . . . . . . 12 ⊢ (𝑋 ≠ 𝑥 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) = (𝐺‘𝑥))
49	47, 48	syl 17	. . . . . . . . . . 11 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) = (𝐺‘𝑥))
50		nelne2 3037	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑦 ≠ 𝑋)
51	50	necomd 2993	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑋 ≠ 𝑦)
52	51	expcom 413	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑋 ∈ 𝐴 → (𝑦 ∈ 𝐴 → 𝑋 ≠ 𝑦))
53	7, 52	sylbi 217	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∉ 𝐴 → (𝑦 ∈ 𝐴 → 𝑋 ≠ 𝑦))
54	53	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵) → (𝑦 ∈ 𝐴 → 𝑋 ≠ 𝑦))
55	54	3ad2ant3 1134	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝑦 ∈ 𝐴 → 𝑋 ≠ 𝑦))
56	55	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐴 → 𝑋 ≠ 𝑦))
57	56	imp 406	. . . . . . . . . . . . 13 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑋 ≠ 𝑦)
58	57	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → 𝑋 ≠ 𝑦)
59		fvunsn 7198	. . . . . . . . . . . 12 ⊢ (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) = (𝐺‘𝑦))
60	58, 59	syl 17	. . . . . . . . . . 11 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) = (𝐺‘𝑦))
61	38, 49, 60	3netr4d 3015	. . . . . . . . . 10 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))
62	61	ex 412	. . . . . . . . 9 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
63	62	ralrimiva 3143	. . . . . . . 8 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
64	1	3ad2ant1 1132	. . . . . . . . . . . . . 14 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝐺:𝐴⟶𝐵)
65	64	ffvelcdmda 7103	. . . . . . . . . . . . 13 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ 𝐵)
66		df-nel 3044	. . . . . . . . . . . . . . . . 17 ⊢ (𝑌 ∉ 𝐵 ↔ ¬ 𝑌 ∈ 𝐵)
67	66	biimpi 216	. . . . . . . . . . . . . . . 16 ⊢ (𝑌 ∉ 𝐵 → ¬ 𝑌 ∈ 𝐵)
68	67	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵) → ¬ 𝑌 ∈ 𝐵)
69	68	3ad2ant3 1134	. . . . . . . . . . . . . 14 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ¬ 𝑌 ∈ 𝐵)
70	69	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → ¬ 𝑌 ∈ 𝐵)
71		nelne2 3037	. . . . . . . . . . . . 13 ⊢ (((𝐺‘𝑥) ∈ 𝐵 ∧ ¬ 𝑌 ∈ 𝐵) → (𝐺‘𝑥) ≠ 𝑌)
72	65, 70, 71	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ≠ 𝑌)
73	72	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → (𝐺‘𝑥) ≠ 𝑌)
74		simpr 484	. . . . . . . . . . . . 13 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → 𝑥 ≠ 𝑋)
75	74	necomd 2993	. . . . . . . . . . . 12 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → 𝑋 ≠ 𝑥)
76	75, 48	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) = (𝐺‘𝑥))
77	6	3ad2ant2 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝑋 ∈ 𝑉)
78		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → 𝑌 ∈ 𝑊)
79	78	3ad2ant2 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝑌 ∈ 𝑊)
80		f1odm 6852	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → dom 𝐺 = 𝐴)
81	80	eqcomd 2740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐴 = dom 𝐺)
82	81	eleq2d 2824	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → (𝑋 ∈ 𝐴 ↔ 𝑋 ∈ dom 𝐺))
83	82	notbid 318	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → (¬ 𝑋 ∈ 𝐴 ↔ ¬ 𝑋 ∈ dom 𝐺))
84	7, 83	bitrid 283	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → (𝑋 ∉ 𝐴 ↔ ¬ 𝑋 ∈ dom 𝐺))
85	84	biimpd 229	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → (𝑋 ∉ 𝐴 → ¬ 𝑋 ∈ dom 𝐺))
86	85	adantrd 491	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → ((𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵) → ¬ 𝑋 ∈ dom 𝐺))
87	86	imp 406	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ¬ 𝑋 ∈ dom 𝐺)
88	87	3adant2 1130	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ¬ 𝑋 ∈ dom 𝐺)
89	77, 79, 88	3jca 1127	. . . . . . . . . . . . . 14 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺))
90	89	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺))
91	90	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺))
92		fsnunfv 7206	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) = 𝑌)
93	91, 92	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) = 𝑌)
94	73, 76, 93	3netr4d 3015	. . . . . . . . . 10 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))
95	94	ex 412	. . . . . . . . 9 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝑥 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋)))
96	77	adantr 480	. . . . . . . . . 10 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑋 ∈ 𝑉)
97		neeq2 3001	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑋 → (𝑥 ≠ 𝑦 ↔ 𝑥 ≠ 𝑋))
98		fveq2 6906	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) = ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))
99	98	neeq2d 2998	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑋 → (((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) ↔ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋)))
100	97, 99	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑋 → ((𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑥 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
101	100	ralsng 4679	. . . . . . . . . 10 ⊢ (𝑋 ∈ 𝑉 → (∀𝑦 ∈ {𝑋} (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑥 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
102	96, 101	syl 17	. . . . . . . . 9 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ {𝑋} (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑥 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
103	95, 102	mpbird 257	. . . . . . . 8 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ {𝑋} (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
104		ralun 4207	. . . . . . . 8 ⊢ ((∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ∧ ∀𝑦 ∈ {𝑋} (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))) → ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
105	63, 103, 104	syl2anc 584	. . . . . . 7 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
106	105	ralrimiva 3143	. . . . . 6 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
107	64	ffvelcdmda 7103	. . . . . . . . . . . . . 14 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) → (𝐺‘𝑦) ∈ 𝐵)
108	69	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) → ¬ 𝑌 ∈ 𝐵)
109	107, 108	jca 511	. . . . . . . . . . . . 13 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) → ((𝐺‘𝑦) ∈ 𝐵 ∧ ¬ 𝑌 ∈ 𝐵))
110	109	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → ((𝐺‘𝑦) ∈ 𝐵 ∧ ¬ 𝑌 ∈ 𝐵))
111		nelne2 3037	. . . . . . . . . . . . 13 ⊢ (((𝐺‘𝑦) ∈ 𝐵 ∧ ¬ 𝑌 ∈ 𝐵) → (𝐺‘𝑦) ≠ 𝑌)
112	111	necomd 2993	. . . . . . . . . . . 12 ⊢ (((𝐺‘𝑦) ∈ 𝐵 ∧ ¬ 𝑌 ∈ 𝐵) → 𝑌 ≠ (𝐺‘𝑦))
113	110, 112	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → 𝑌 ≠ (𝐺‘𝑦))
114	89	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺))
115	114	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺))
116	115, 92	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) = 𝑌)
117	59	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) = (𝐺‘𝑦))
118	113, 116, 117	3netr4d 3015	. . . . . . . . . 10 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))
119	118	ex 412	. . . . . . . . 9 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) → (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
120	119	ralrimiva 3143	. . . . . . . 8 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑦 ∈ 𝐴 (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
121		eqid 2734	. . . . . . . . . 10 ⊢ 𝑋 = 𝑋
122		eqneqall 2948	. . . . . . . . . 10 ⊢ (𝑋 = 𝑋 → (𝑋 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋)))
123	121, 122	ax-mp 5	. . . . . . . . 9 ⊢ (𝑋 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))
124		neeq2 3001	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑋 → (𝑋 ≠ 𝑦 ↔ 𝑋 ≠ 𝑋))
125	98	neeq2d 2998	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑋 → (((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) ↔ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋)))
126	124, 125	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑋 → ((𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑋 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
127	126	ralsng 4679	. . . . . . . . . 10 ⊢ (𝑋 ∈ 𝑉 → (∀𝑦 ∈ {𝑋} (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑋 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
128	77, 127	syl 17	. . . . . . . . 9 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (∀𝑦 ∈ {𝑋} (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑋 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
129	123, 128	mpbiri 258	. . . . . . . 8 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑦 ∈ {𝑋} (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
130		ralun 4207	. . . . . . . 8 ⊢ ((∀𝑦 ∈ 𝐴 (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ∧ ∀𝑦 ∈ {𝑋} (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))) → ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
131	120, 129, 130	syl2anc 584	. . . . . . 7 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
132		neeq1 3000	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝑥 ≠ 𝑦 ↔ 𝑋 ≠ 𝑦))
133		fveq2 6906	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) = ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))
134	133	neeq1d 2997	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) ↔ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
135	132, 134	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → ((𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
136	135	ralbidv 3175	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
137	136	ralsng 4679	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑉 → (∀𝑥 ∈ {𝑋}∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
138	77, 137	syl 17	. . . . . . 7 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (∀𝑥 ∈ {𝑋}∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
139	131, 138	mpbird 257	. . . . . 6 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑥 ∈ {𝑋}∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
140		ralun 4207	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ∧ ∀𝑥 ∈ {𝑋}∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))) → ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
141	106, 139, 140	syl2anc 584	. . . . 5 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
142	20, 141	jca 511	. . . 4 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}) ∧ ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
143		rnun 6167	. . . . 5 ⊢ ran (𝐺 ∪ {⟨𝑋, 𝑌⟩}) = (ran 𝐺 ∪ ran {⟨𝑋, 𝑌⟩})
144		f1ofo 6855	. . . . . . . 8 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐺:𝐴–onto→𝐵)
145		forn 6823	. . . . . . . 8 ⊢ (𝐺:𝐴–onto→𝐵 → ran 𝐺 = 𝐵)
146	144, 145	syl 17	. . . . . . 7 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → ran 𝐺 = 𝐵)
147	146	3ad2ant1 1132	. . . . . 6 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ran 𝐺 = 𝐵)
148		rnsnopg 6242	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑉 → ran {⟨𝑋, 𝑌⟩} = {𝑌})
149	148	adantr 480	. . . . . . 7 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ran {⟨𝑋, 𝑌⟩} = {𝑌})
150	149	3ad2ant2 1133	. . . . . 6 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ran {⟨𝑋, 𝑌⟩} = {𝑌})
151	147, 150	uneq12d 4178	. . . . 5 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (ran 𝐺 ∪ ran {⟨𝑋, 𝑌⟩}) = (𝐵 ∪ {𝑌}))
152	143, 151	eqtrid 2786	. . . 4 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ran (𝐺 ∪ {⟨𝑋, 𝑌⟩}) = (𝐵 ∪ {𝑌}))
153	142, 152	jca 511	. . 3 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}) ∧ ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))) ∧ ran (𝐺 ∪ {⟨𝑋, 𝑌⟩}) = (𝐵 ∪ {𝑌})))
154		dff1o5 6857	. . . 4 ⊢ ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}) ↔ ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1→(𝐵 ∪ {𝑌}) ∧ ran (𝐺 ∪ {⟨𝑋, 𝑌⟩}) = (𝐵 ∪ {𝑌})))
155		dff14a 7289	. . . 4 ⊢ ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1→(𝐵 ∪ {𝑌}) ↔ ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}) ∧ ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
156	154, 155	bianbi 627	. . 3 ⊢ ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}) ↔ (((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}) ∧ ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))) ∧ ran (𝐺 ∪ {⟨𝑋, 𝑌⟩}) = (𝐵 ∪ {𝑌})))
157	153, 156	sylibr 234	. 2 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}))
158		f1ounsn.f	. . 3 ⊢ 𝐹 = (𝐺 ∪ {⟨𝑋, 𝑌⟩})
159		f1oeq1 6836	. . 3 ⊢ (𝐹 = (𝐺 ∪ {⟨𝑋, 𝑌⟩}) → (𝐹:(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}) ↔ (𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌})))
160	158, 159	ax-mp 5	. 2 ⊢ (𝐹:(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}) ↔ (𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}))
161	157, 160	sylibr 234	1 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝐹:(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1536 ∈ wcel 2105 ≠ wne 2937 ∉ wnel 3043 ∀wral 3058 ∪ cun 3960 ⊆ wss 3962 {csn 4630 ⟨cop 4636 dom cdm 5688 ran crn 5689 ⟶wf 6558 –1-1→wf1 6559 –onto→wfo 6560 –1-1-onto→wf1o 6561 ‘cfv 6562

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pr 5437

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-br 5148 df-opab 5210 df-id 5582 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-iota 6515 df-fun 6564 df-fn 6565 df-f 6566 df-f1 6567 df-fo 6568 df-f1o 6569 df-fv 6570

This theorem is referenced by: isubgr3stgrlem1 47868

W3C validator