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 7258

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 6808	. . . . . . . . 9 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐺:𝐴⟶𝐵)
2		ssun1 4132	. . . . . . . . . 10 ⊢ 𝐵 ⊆ (𝐵 ∪ {𝑌})
3	2	a1i 11	. . . . . . . . 9 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐵 ⊆ (𝐵 ∪ {𝑌}))
4	1, 3	fssd 6711	. . . . . . . 8 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐺:𝐴⟶(𝐵 ∪ {𝑌}))
5	4	3ad2ant1 1147	. . . . . . 7 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝐺:𝐴⟶(𝐵 ∪ {𝑌}))
6		simpl 486	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → 𝑋 ∈ 𝑉)
7		df-nel 3064	. . . . . . . . . . 11 ⊢ (𝑋 ∉ 𝐴 ↔ ¬ 𝑋 ∈ 𝐴)
8	7	biimpi 218	. . . . . . . . . 10 ⊢ (𝑋 ∉ 𝐴 → ¬ 𝑋 ∈ 𝐴)
9	8	adantr 484	. . . . . . . . 9 ⊢ ((𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵) → ¬ 𝑋 ∈ 𝐴)
10	6, 9	anim12i 622	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝐴))
11	10	3adant1 1144	. . . . . . 7 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝐴))
12		eqid 2764	. . . . . . . . . . 11 ⊢ 𝑌 = 𝑌
13	12	olci 877	. . . . . . . . . 10 ⊢ (𝑌 ∈ 𝐵 ∨ 𝑌 = 𝑌)
14		elunsn 4644	. . . . . . . . . 10 ⊢ (𝑌 ∈ 𝑊 → (𝑌 ∈ (𝐵 ∪ {𝑌}) ↔ (𝑌 ∈ 𝐵 ∨ 𝑌 = 𝑌)))
15	13, 14	mpbiri 260	. . . . . . . . 9 ⊢ (𝑌 ∈ 𝑊 → 𝑌 ∈ (𝐵 ∪ {𝑌}))
16	15	adantl 485	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → 𝑌 ∈ (𝐵 ∪ {𝑌}))
17	16	3ad2ant2 1148	. . . . . . 7 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝑌 ∈ (𝐵 ∪ {𝑌}))
18	5, 11, 17	3jca 1142	. . . . . 6 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝐺:𝐴⟶(𝐵 ∪ {𝑌}) ∧ (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝐴) ∧ 𝑌 ∈ (𝐵 ∪ {𝑌})))
19		fsnunf 7171	. . . . . 6 ⊢ ((𝐺:𝐴⟶(𝐵 ∪ {𝑌}) ∧ (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝐴) ∧ 𝑌 ∈ (𝐵 ∪ {𝑌})) → (𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}))
20	18, 19	syl 17	. . . . 5 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}))
21		f1of1 6807	. . . . . . . . . . . . . . 15 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐺:𝐴–1-1→𝐵)
22		dff14a 7256	. . . . . . . . . . . . . . . 16 ⊢ (𝐺:𝐴–1-1→𝐵 ↔ (𝐺:𝐴⟶𝐵 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎 ≠ 𝑏 → (𝐺‘𝑎) ≠ (𝐺‘𝑏))))
23		neeq1 3021	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑥 → (𝑎 ≠ 𝑏 ↔ 𝑥 ≠ 𝑏))
24		fveq2 6869	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑥 → (𝐺‘𝑎) = (𝐺‘𝑥))
25	24	neeq1d 3018	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑥 → ((𝐺‘𝑎) ≠ (𝐺‘𝑏) ↔ (𝐺‘𝑥) ≠ (𝐺‘𝑏)))
26	23, 25	imbi12d 346	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑥 → ((𝑎 ≠ 𝑏 → (𝐺‘𝑎) ≠ (𝐺‘𝑏)) ↔ (𝑥 ≠ 𝑏 → (𝐺‘𝑥) ≠ (𝐺‘𝑏))))
27		neeq2 3022	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = 𝑦 → (𝑥 ≠ 𝑏 ↔ 𝑥 ≠ 𝑦))
28		fveq2 6869	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = 𝑦 → (𝐺‘𝑏) = (𝐺‘𝑦))
29	28	neeq2d 3019	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = 𝑦 → ((𝐺‘𝑥) ≠ (𝐺‘𝑏) ↔ (𝐺‘𝑥) ≠ (𝐺‘𝑦)))
30	27, 29	imbi12d 346	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 𝑦 → ((𝑥 ≠ 𝑏 → (𝐺‘𝑥) ≠ (𝐺‘𝑏)) ↔ (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
31	26, 30	rspc2va 3595	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎 ≠ 𝑏 → (𝐺‘𝑎) ≠ (𝐺‘𝑏))) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)))
32	31	expcom 417	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎 ≠ 𝑏 → (𝐺‘𝑎) ≠ (𝐺‘𝑏)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
33	32	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺:𝐴⟶𝐵 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎 ≠ 𝑏 → (𝐺‘𝑎) ≠ (𝐺‘𝑏))) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
34	22, 33	sylbi 219	. . . . . . . . . . . . . . 15 ⊢ (𝐺:𝐴–1-1→𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
35	21, 34	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
36	35	3ad2ant1 1147	. . . . . . . . . . . . 13 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
37	36	impl 459	. . . . . . . . . . . 12 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)))
38	37	imp 410	. . . . . . . . . . 11 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → (𝐺‘𝑥) ≠ (𝐺‘𝑦))
39		nelne2 3057	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑥 ≠ 𝑋)
40	39	necomd 3014	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑋 ≠ 𝑥)
41	40	expcom 417	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑋 ∈ 𝐴 → (𝑥 ∈ 𝐴 → 𝑋 ≠ 𝑥))
42	7, 41	sylbi 219	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∉ 𝐴 → (𝑥 ∈ 𝐴 → 𝑋 ≠ 𝑥))
43	42	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵) → (𝑥 ∈ 𝐴 → 𝑋 ≠ 𝑥))
44	43	3ad2ant3 1149	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝑥 ∈ 𝐴 → 𝑋 ≠ 𝑥))
45	44	imp 410	. . . . . . . . . . . . . 14 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑋 ≠ 𝑥)
46	45	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑋 ≠ 𝑥)
47	46	adantr 484	. . . . . . . . . . . 12 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → 𝑋 ≠ 𝑥)
48		fvunsn 7165	. . . . . . . . . . . 12 ⊢ (𝑋 ≠ 𝑥 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) = (𝐺‘𝑥))
49	47, 48	syl 17	. . . . . . . . . . 11 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) = (𝐺‘𝑥))
50		nelne2 3057	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑦 ≠ 𝑋)
51	50	necomd 3014	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑋 ≠ 𝑦)
52	51	expcom 417	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑋 ∈ 𝐴 → (𝑦 ∈ 𝐴 → 𝑋 ≠ 𝑦))
53	7, 52	sylbi 219	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∉ 𝐴 → (𝑦 ∈ 𝐴 → 𝑋 ≠ 𝑦))
54	53	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵) → (𝑦 ∈ 𝐴 → 𝑋 ≠ 𝑦))
55	54	3ad2ant3 1149	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝑦 ∈ 𝐴 → 𝑋 ≠ 𝑦))
56	55	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐴 → 𝑋 ≠ 𝑦))
57	56	imp 410	. . . . . . . . . . . . 13 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑋 ≠ 𝑦)
58	57	adantr 484	. . . . . . . . . . . 12 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → 𝑋 ≠ 𝑦)
59		fvunsn 7165	. . . . . . . . . . . 12 ⊢ (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) = (𝐺‘𝑦))
60	58, 59	syl 17	. . . . . . . . . . 11 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) = (𝐺‘𝑦))
61	38, 49, 60	3netr4d 3036	. . . . . . . . . 10 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))
62	61	ex 416	. . . . . . . . 9 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
63	62	ralrimiva 3156	. . . . . . . 8 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
64	1	3ad2ant1 1147	. . . . . . . . . . . . . 14 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝐺:𝐴⟶𝐵)
65	64	ffvelcdmda 7067	. . . . . . . . . . . . 13 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ 𝐵)
66		df-nel 3064	. . . . . . . . . . . . . . . . 17 ⊢ (𝑌 ∉ 𝐵 ↔ ¬ 𝑌 ∈ 𝐵)
67	66	biimpi 218	. . . . . . . . . . . . . . . 16 ⊢ (𝑌 ∉ 𝐵 → ¬ 𝑌 ∈ 𝐵)
68	67	adantl 485	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵) → ¬ 𝑌 ∈ 𝐵)
69	68	3ad2ant3 1149	. . . . . . . . . . . . . 14 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ¬ 𝑌 ∈ 𝐵)
70	69	adantr 484	. . . . . . . . . . . . 13 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → ¬ 𝑌 ∈ 𝐵)
71		nelne2 3057	. . . . . . . . . . . . 13 ⊢ (((𝐺‘𝑥) ∈ 𝐵 ∧ ¬ 𝑌 ∈ 𝐵) → (𝐺‘𝑥) ≠ 𝑌)
72	65, 70, 71	syl2anc 593	. . . . . . . . . . . 12 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ≠ 𝑌)
73	72	adantr 484	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → (𝐺‘𝑥) ≠ 𝑌)
74		simpr 488	. . . . . . . . . . . . 13 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → 𝑥 ≠ 𝑋)
75	74	necomd 3014	. . . . . . . . . . . 12 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → 𝑋 ≠ 𝑥)
76	75, 48	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) = (𝐺‘𝑥))
77	6	3ad2ant2 1148	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝑋 ∈ 𝑉)
78		simpr 488	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → 𝑌 ∈ 𝑊)
79	78	3ad2ant2 1148	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝑌 ∈ 𝑊)
80		f1odm 6812	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → dom 𝐺 = 𝐴)
81	80	eqcomd 2770	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐴 = dom 𝐺)
82	81	eleq2d 2850	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → (𝑋 ∈ 𝐴 ↔ 𝑋 ∈ dom 𝐺))
83	82	notbid 320	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → (¬ 𝑋 ∈ 𝐴 ↔ ¬ 𝑋 ∈ dom 𝐺))
84	7, 83	bitrid 285	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → (𝑋 ∉ 𝐴 ↔ ¬ 𝑋 ∈ dom 𝐺))
85	84	biimpd 231	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → (𝑋 ∉ 𝐴 → ¬ 𝑋 ∈ dom 𝐺))
86	85	adantrd 495	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → ((𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵) → ¬ 𝑋 ∈ dom 𝐺))
87	86	imp 410	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ¬ 𝑋 ∈ dom 𝐺)
88	87	3adant2 1145	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ¬ 𝑋 ∈ dom 𝐺)
89	77, 79, 88	3jca 1142	. . . . . . . . . . . . . 14 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺))
90	89	adantr 484	. . . . . . . . . . . . 13 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺))
91	90	adantr 484	. . . . . . . . . . . 12 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺))
92		fsnunfv 7173	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) = 𝑌)
93	91, 92	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) = 𝑌)
94	73, 76, 93	3netr4d 3036	. . . . . . . . . 10 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))
95	94	ex 416	. . . . . . . . 9 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝑥 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋)))
96	77	adantr 484	. . . . . . . . . 10 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑋 ∈ 𝑉)
97		neeq2 3022	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑋 → (𝑥 ≠ 𝑦 ↔ 𝑥 ≠ 𝑋))
98		fveq2 6869	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) = ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))
99	98	neeq2d 3019	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑋 → (((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) ↔ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋)))
100	97, 99	imbi12d 346	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑋 → ((𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑥 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
101	100	ralsng 4636	. . . . . . . . . 10 ⊢ (𝑋 ∈ 𝑉 → (∀𝑦 ∈ {𝑋} (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑥 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
102	96, 101	syl 17	. . . . . . . . 9 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ {𝑋} (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑥 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
103	95, 102	mpbird 259	. . . . . . . 8 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ {𝑋} (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
104		ralun 4152	. . . . . . . 8 ⊢ ((∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ∧ ∀𝑦 ∈ {𝑋} (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))) → ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
105	63, 103, 104	syl2anc 593	. . . . . . 7 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
106	105	ralrimiva 3156	. . . . . 6 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
107	64	ffvelcdmda 7067	. . . . . . . . . . . . . 14 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) → (𝐺‘𝑦) ∈ 𝐵)
108	69	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) → ¬ 𝑌 ∈ 𝐵)
109	107, 108	jca 519	. . . . . . . . . . . . 13 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) → ((𝐺‘𝑦) ∈ 𝐵 ∧ ¬ 𝑌 ∈ 𝐵))
110	109	adantr 484	. . . . . . . . . . . 12 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → ((𝐺‘𝑦) ∈ 𝐵 ∧ ¬ 𝑌 ∈ 𝐵))
111		nelne2 3057	. . . . . . . . . . . . 13 ⊢ (((𝐺‘𝑦) ∈ 𝐵 ∧ ¬ 𝑌 ∈ 𝐵) → (𝐺‘𝑦) ≠ 𝑌)
112	111	necomd 3014	. . . . . . . . . . . 12 ⊢ (((𝐺‘𝑦) ∈ 𝐵 ∧ ¬ 𝑌 ∈ 𝐵) → 𝑌 ≠ (𝐺‘𝑦))
113	110, 112	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → 𝑌 ≠ (𝐺‘𝑦))
114	89	adantr 484	. . . . . . . . . . . . 13 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺))
115	114	adantr 484	. . . . . . . . . . . 12 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺))
116	115, 92	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) = 𝑌)
117	59	adantl 485	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) = (𝐺‘𝑦))
118	113, 116, 117	3netr4d 3036	. . . . . . . . . 10 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))
119	118	ex 416	. . . . . . . . 9 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) → (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
120	119	ralrimiva 3156	. . . . . . . 8 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑦 ∈ 𝐴 (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
121		eqid 2764	. . . . . . . . . 10 ⊢ 𝑋 = 𝑋
122		eqneqall 2970	. . . . . . . . . 10 ⊢ (𝑋 = 𝑋 → (𝑋 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋)))
123	121, 122	ax-mp 5	. . . . . . . . 9 ⊢ (𝑋 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))
124		neeq2 3022	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑋 → (𝑋 ≠ 𝑦 ↔ 𝑋 ≠ 𝑋))
125	98	neeq2d 3019	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑋 → (((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) ↔ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋)))
126	124, 125	imbi12d 346	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑋 → ((𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑋 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
127	126	ralsng 4636	. . . . . . . . . 10 ⊢ (𝑋 ∈ 𝑉 → (∀𝑦 ∈ {𝑋} (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑋 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
128	77, 127	syl 17	. . . . . . . . 9 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (∀𝑦 ∈ {𝑋} (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑋 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
129	123, 128	mpbiri 260	. . . . . . . 8 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑦 ∈ {𝑋} (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
130		ralun 4152	. . . . . . . 8 ⊢ ((∀𝑦 ∈ 𝐴 (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ∧ ∀𝑦 ∈ {𝑋} (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))) → ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
131	120, 129, 130	syl2anc 593	. . . . . . 7 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
132		neeq1 3021	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝑥 ≠ 𝑦 ↔ 𝑋 ≠ 𝑦))
133		fveq2 6869	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) = ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))
134	133	neeq1d 3018	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) ↔ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
135	132, 134	imbi12d 346	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → ((𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
136	135	ralbidv 3187	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
137	136	ralsng 4636	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑉 → (∀𝑥 ∈ {𝑋}∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
138	77, 137	syl 17	. . . . . . 7 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (∀𝑥 ∈ {𝑋}∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
139	131, 138	mpbird 259	. . . . . 6 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑥 ∈ {𝑋}∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
140		ralun 4152	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ∧ ∀𝑥 ∈ {𝑋}∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))) → ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
141	106, 139, 140	syl2anc 593	. . . . 5 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
142	20, 141	jca 519	. . . 4 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}) ∧ ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
143		rnun 6131	. . . . 5 ⊢ ran (𝐺 ∪ {⟨𝑋, 𝑌⟩}) = (ran 𝐺 ∪ ran {⟨𝑋, 𝑌⟩})
144		f1ofo 6816	. . . . . . . 8 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐺:𝐴–onto→𝐵)
145		forn 6783	. . . . . . . 8 ⊢ (𝐺:𝐴–onto→𝐵 → ran 𝐺 = 𝐵)
146	144, 145	syl 17	. . . . . . 7 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → ran 𝐺 = 𝐵)
147	146	3ad2ant1 1147	. . . . . 6 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ran 𝐺 = 𝐵)
148		rnsnopg 6210	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑉 → ran {⟨𝑋, 𝑌⟩} = {𝑌})
149	148	adantr 484	. . . . . . 7 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ran {⟨𝑋, 𝑌⟩} = {𝑌})
150	149	3ad2ant2 1148	. . . . . 6 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ran {⟨𝑋, 𝑌⟩} = {𝑌})
151	147, 150	uneq12d 4124	. . . . 5 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (ran 𝐺 ∪ ran {⟨𝑋, 𝑌⟩}) = (𝐵 ∪ {𝑌}))
152	143, 151	eqtrid 2811	. . . 4 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ran (𝐺 ∪ {⟨𝑋, 𝑌⟩}) = (𝐵 ∪ {𝑌}))
153	142, 152	jca 519	. . 3 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}) ∧ ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))) ∧ ran (𝐺 ∪ {⟨𝑋, 𝑌⟩}) = (𝐵 ∪ {𝑌})))
154		dff1o5 6818	. . . 4 ⊢ ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}) ↔ ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1→(𝐵 ∪ {𝑌}) ∧ ran (𝐺 ∪ {⟨𝑋, 𝑌⟩}) = (𝐵 ∪ {𝑌})))
155		dff14a 7256	. . . 4 ⊢ ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1→(𝐵 ∪ {𝑌}) ↔ ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}) ∧ ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
156	154, 155	bianbi 636	. . 3 ⊢ ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}) ↔ (((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}) ∧ ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))) ∧ ran (𝐺 ∪ {⟨𝑋, 𝑌⟩}) = (𝐵 ∪ {𝑌})))
157	153, 156	sylibr 236	. 2 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}))
158		f1ounsn.f	. . 3 ⊢ 𝐹 = (𝐺 ∪ {⟨𝑋, 𝑌⟩})
159		f1oeq1 6796	. . 3 ⊢ (𝐹 = (𝐺 ∪ {⟨𝑋, 𝑌⟩}) → (𝐹:(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}) ↔ (𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌})))
160	158, 159	ax-mp 5	. 2 ⊢ (𝐹:(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}) ↔ (𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}))
161	157, 160	sylibr 236	1 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝐹:(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 ∧ w3a 1099 = wceq 1562 ∈ wcel 2144 ≠ wne 2959 ∉ wnel 3063 ∀wral 3078 ∪ cun 3904 ⊆ wss 3906 {csn 4584 ⟨cop 4590 dom cdm 5649 ran crn 5650 ⟶wf 6519 –1-1→wf1 6520 –onto→wfo 6521 –1-1-onto→wf1o 6522 ‘cfv 6523

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1817 ax-4 1831 ax-5 1932 ax-6 1989 ax-7 2030 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2214 ax-ext 2736 ax-sep 5248 ax-nul 5258 ax-pr 5392

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1101 df-tru 1565 df-fal 1575 df-ex 1802 df-nf 1806 df-sb 2093 df-mo 2568 df-eu 2598 df-clab 2743 df-cleq 2756 df-clel 2839 df-ne 2960 df-nel 3064 df-ral 3079 df-rex 3089 df-rab 3417 df-v 3458 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4288 df-if 4483 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-br 5103 df-opab 5165 df-id 5544 df-xp 5655 df-rel 5656 df-cnv 5657 df-co 5658 df-dm 5659 df-rn 5660 df-res 5661 df-iota 6479 df-fun 6525 df-fn 6526 df-f 6527 df-f1 6528 df-fo 6529 df-f1o 6530 df-fv 6531

This theorem is referenced by: isubgr3stgrlem1 48593

W3C validator