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 7220

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 6771	. . . . . . . . 9 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐺:𝐴⟶𝐵)
2		ssun1 4110	. . . . . . . . . 10 ⊢ 𝐵 ⊆ (𝐵 ∪ {𝑌})
3	2	a1i 11	. . . . . . . . 9 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐵 ⊆ (𝐵 ∪ {𝑌}))
4	1, 3	fssd 6676	. . . . . . . 8 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐺:𝐴⟶(𝐵 ∪ {𝑌}))
5	4	3ad2ant1 1140	. . . . . . 7 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝐺:𝐴⟶(𝐵 ∪ {𝑌}))
6		simpl 484	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → 𝑋 ∈ 𝑉)
7		df-nel 3041	. . . . . . . . . . 11 ⊢ (𝑋 ∉ 𝐴 ↔ ¬ 𝑋 ∈ 𝐴)
8	7	biimpi 218	. . . . . . . . . 10 ⊢ (𝑋 ∉ 𝐴 → ¬ 𝑋 ∈ 𝐴)
9	8	adantr 482	. . . . . . . . 9 ⊢ ((𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵) → ¬ 𝑋 ∈ 𝐴)
10	6, 9	anim12i 620	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝐴))
11	10	3adant1 1137	. . . . . . 7 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝐴))
12		eqid 2741	. . . . . . . . . . 11 ⊢ 𝑌 = 𝑌
13	12	olci 873	. . . . . . . . . 10 ⊢ (𝑌 ∈ 𝐵 ∨ 𝑌 = 𝑌)
14		elunsn 4618	. . . . . . . . . 10 ⊢ (𝑌 ∈ 𝑊 → (𝑌 ∈ (𝐵 ∪ {𝑌}) ↔ (𝑌 ∈ 𝐵 ∨ 𝑌 = 𝑌)))
15	13, 14	mpbiri 260	. . . . . . . . 9 ⊢ (𝑌 ∈ 𝑊 → 𝑌 ∈ (𝐵 ∪ {𝑌}))
16	15	adantl 483	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → 𝑌 ∈ (𝐵 ∪ {𝑌}))
17	16	3ad2ant2 1141	. . . . . . 7 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝑌 ∈ (𝐵 ∪ {𝑌}))
18	5, 11, 17	3jca 1135	. . . . . 6 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝐺:𝐴⟶(𝐵 ∪ {𝑌}) ∧ (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝐴) ∧ 𝑌 ∈ (𝐵 ∪ {𝑌})))
19		fsnunf 7133	. . . . . 6 ⊢ ((𝐺:𝐴⟶(𝐵 ∪ {𝑌}) ∧ (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝐴) ∧ 𝑌 ∈ (𝐵 ∪ {𝑌})) → (𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}))
20	18, 19	syl 17	. . . . 5 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}))
21		f1of1 6770	. . . . . . . . . . . . . . 15 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐺:𝐴–1-1→𝐵)
22		dff14a 7218	. . . . . . . . . . . . . . . 16 ⊢ (𝐺:𝐴–1-1→𝐵 ↔ (𝐺:𝐴⟶𝐵 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎 ≠ 𝑏 → (𝐺‘𝑎) ≠ (𝐺‘𝑏))))
23		neeq1 2998	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑥 → (𝑎 ≠ 𝑏 ↔ 𝑥 ≠ 𝑏))
24		fveq2 6831	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑥 → (𝐺‘𝑎) = (𝐺‘𝑥))
25	24	neeq1d 2995	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑥 → ((𝐺‘𝑎) ≠ (𝐺‘𝑏) ↔ (𝐺‘𝑥) ≠ (𝐺‘𝑏)))
26	23, 25	imbi12d 346	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑥 → ((𝑎 ≠ 𝑏 → (𝐺‘𝑎) ≠ (𝐺‘𝑏)) ↔ (𝑥 ≠ 𝑏 → (𝐺‘𝑥) ≠ (𝐺‘𝑏))))
27		neeq2 2999	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = 𝑦 → (𝑥 ≠ 𝑏 ↔ 𝑥 ≠ 𝑦))
28		fveq2 6831	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = 𝑦 → (𝐺‘𝑏) = (𝐺‘𝑦))
29	28	neeq2d 2996	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = 𝑦 → ((𝐺‘𝑥) ≠ (𝐺‘𝑏) ↔ (𝐺‘𝑥) ≠ (𝐺‘𝑦)))
30	27, 29	imbi12d 346	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 𝑦 → ((𝑥 ≠ 𝑏 → (𝐺‘𝑥) ≠ (𝐺‘𝑏)) ↔ (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
31	26, 30	rspc2va 3574	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎 ≠ 𝑏 → (𝐺‘𝑎) ≠ (𝐺‘𝑏))) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)))
32	31	expcom 415	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎 ≠ 𝑏 → (𝐺‘𝑎) ≠ (𝐺‘𝑏)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
33	32	adantl 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺:𝐴⟶𝐵 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎 ≠ 𝑏 → (𝐺‘𝑎) ≠ (𝐺‘𝑏))) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
34	22, 33	sylbi 219	. . . . . . . . . . . . . . 15 ⊢ (𝐺:𝐴–1-1→𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
35	21, 34	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
36	35	3ad2ant1 1140	. . . . . . . . . . . . 13 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
37	36	impl 457	. . . . . . . . . . . 12 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)))
38	37	imp 408	. . . . . . . . . . 11 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → (𝐺‘𝑥) ≠ (𝐺‘𝑦))
39		nelne2 3034	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑥 ≠ 𝑋)
40	39	necomd 2991	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑋 ≠ 𝑥)
41	40	expcom 415	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑋 ∈ 𝐴 → (𝑥 ∈ 𝐴 → 𝑋 ≠ 𝑥))
42	7, 41	sylbi 219	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∉ 𝐴 → (𝑥 ∈ 𝐴 → 𝑋 ≠ 𝑥))
43	42	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵) → (𝑥 ∈ 𝐴 → 𝑋 ≠ 𝑥))
44	43	3ad2ant3 1142	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝑥 ∈ 𝐴 → 𝑋 ≠ 𝑥))
45	44	imp 408	. . . . . . . . . . . . . 14 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑋 ≠ 𝑥)
46	45	adantr 482	. . . . . . . . . . . . 13 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑋 ≠ 𝑥)
47	46	adantr 482	. . . . . . . . . . . 12 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → 𝑋 ≠ 𝑥)
48		fvunsn 7127	. . . . . . . . . . . 12 ⊢ (𝑋 ≠ 𝑥 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) = (𝐺‘𝑥))
49	47, 48	syl 17	. . . . . . . . . . 11 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) = (𝐺‘𝑥))
50		nelne2 3034	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑦 ≠ 𝑋)
51	50	necomd 2991	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑋 ≠ 𝑦)
52	51	expcom 415	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑋 ∈ 𝐴 → (𝑦 ∈ 𝐴 → 𝑋 ≠ 𝑦))
53	7, 52	sylbi 219	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∉ 𝐴 → (𝑦 ∈ 𝐴 → 𝑋 ≠ 𝑦))
54	53	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵) → (𝑦 ∈ 𝐴 → 𝑋 ≠ 𝑦))
55	54	3ad2ant3 1142	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝑦 ∈ 𝐴 → 𝑋 ≠ 𝑦))
56	55	adantr 482	. . . . . . . . . . . . . 14 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐴 → 𝑋 ≠ 𝑦))
57	56	imp 408	. . . . . . . . . . . . 13 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑋 ≠ 𝑦)
58	57	adantr 482	. . . . . . . . . . . 12 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → 𝑋 ≠ 𝑦)
59		fvunsn 7127	. . . . . . . . . . . 12 ⊢ (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) = (𝐺‘𝑦))
60	58, 59	syl 17	. . . . . . . . . . 11 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) = (𝐺‘𝑦))
61	38, 49, 60	3netr4d 3013	. . . . . . . . . 10 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))
62	61	ex 414	. . . . . . . . 9 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
63	62	ralrimiva 3133	. . . . . . . 8 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
64	1	3ad2ant1 1140	. . . . . . . . . . . . . 14 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝐺:𝐴⟶𝐵)
65	64	ffvelcdmda 7029	. . . . . . . . . . . . 13 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ 𝐵)
66		df-nel 3041	. . . . . . . . . . . . . . . . 17 ⊢ (𝑌 ∉ 𝐵 ↔ ¬ 𝑌 ∈ 𝐵)
67	66	biimpi 218	. . . . . . . . . . . . . . . 16 ⊢ (𝑌 ∉ 𝐵 → ¬ 𝑌 ∈ 𝐵)
68	67	adantl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵) → ¬ 𝑌 ∈ 𝐵)
69	68	3ad2ant3 1142	. . . . . . . . . . . . . 14 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ¬ 𝑌 ∈ 𝐵)
70	69	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → ¬ 𝑌 ∈ 𝐵)
71		nelne2 3034	. . . . . . . . . . . . 13 ⊢ (((𝐺‘𝑥) ∈ 𝐵 ∧ ¬ 𝑌 ∈ 𝐵) → (𝐺‘𝑥) ≠ 𝑌)
72	65, 70, 71	syl2anc 591	. . . . . . . . . . . 12 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ≠ 𝑌)
73	72	adantr 482	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → (𝐺‘𝑥) ≠ 𝑌)
74		simpr 486	. . . . . . . . . . . . 13 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → 𝑥 ≠ 𝑋)
75	74	necomd 2991	. . . . . . . . . . . 12 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → 𝑋 ≠ 𝑥)
76	75, 48	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) = (𝐺‘𝑥))
77	6	3ad2ant2 1141	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝑋 ∈ 𝑉)
78		simpr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → 𝑌 ∈ 𝑊)
79	78	3ad2ant2 1141	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝑌 ∈ 𝑊)
80		f1odm 6775	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → dom 𝐺 = 𝐴)
81	80	eqcomd 2747	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐴 = dom 𝐺)
82	81	eleq2d 2827	. . . . . . . . . . . . . . . . . . . . 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 493	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → ((𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵) → ¬ 𝑋 ∈ dom 𝐺))
87	86	imp 408	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ¬ 𝑋 ∈ dom 𝐺)
88	87	3adant2 1138	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ¬ 𝑋 ∈ dom 𝐺)
89	77, 79, 88	3jca 1135	. . . . . . . . . . . . . 14 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺))
90	89	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺))
91	90	adantr 482	. . . . . . . . . . . 12 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺))
92		fsnunfv 7135	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) = 𝑌)
93	91, 92	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) = 𝑌)
94	73, 76, 93	3netr4d 3013	. . . . . . . . . 10 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))
95	94	ex 414	. . . . . . . . 9 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝑥 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋)))
96	77	adantr 482	. . . . . . . . . 10 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑋 ∈ 𝑉)
97		neeq2 2999	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑋 → (𝑥 ≠ 𝑦 ↔ 𝑥 ≠ 𝑋))
98		fveq2 6831	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) = ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))
99	98	neeq2d 2996	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑋 → (((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) ↔ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋)))
100	97, 99	imbi12d 346	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑋 → ((𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑥 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
101	100	ralsng 4610	. . . . . . . . . 10 ⊢ (𝑋 ∈ 𝑉 → (∀𝑦 ∈ {𝑋} (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑥 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
102	96, 101	syl 17	. . . . . . . . 9 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ {𝑋} (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑥 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
103	95, 102	mpbird 259	. . . . . . . 8 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ {𝑋} (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
104		ralun 4130	. . . . . . . 8 ⊢ ((∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ∧ ∀𝑦 ∈ {𝑋} (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))) → ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
105	63, 103, 104	syl2anc 591	. . . . . . 7 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
106	105	ralrimiva 3133	. . . . . 6 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
107	64	ffvelcdmda 7029	. . . . . . . . . . . . . 14 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) → (𝐺‘𝑦) ∈ 𝐵)
108	69	adantr 482	. . . . . . . . . . . . . 14 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) → ¬ 𝑌 ∈ 𝐵)
109	107, 108	jca 517	. . . . . . . . . . . . 13 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) → ((𝐺‘𝑦) ∈ 𝐵 ∧ ¬ 𝑌 ∈ 𝐵))
110	109	adantr 482	. . . . . . . . . . . 12 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → ((𝐺‘𝑦) ∈ 𝐵 ∧ ¬ 𝑌 ∈ 𝐵))
111		nelne2 3034	. . . . . . . . . . . . 13 ⊢ (((𝐺‘𝑦) ∈ 𝐵 ∧ ¬ 𝑌 ∈ 𝐵) → (𝐺‘𝑦) ≠ 𝑌)
112	111	necomd 2991	. . . . . . . . . . . 12 ⊢ (((𝐺‘𝑦) ∈ 𝐵 ∧ ¬ 𝑌 ∈ 𝐵) → 𝑌 ≠ (𝐺‘𝑦))
113	110, 112	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → 𝑌 ≠ (𝐺‘𝑦))
114	89	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺))
115	114	adantr 482	. . . . . . . . . . . 12 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺))
116	115, 92	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) = 𝑌)
117	59	adantl 483	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) = (𝐺‘𝑦))
118	113, 116, 117	3netr4d 3013	. . . . . . . . . 10 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))
119	118	ex 414	. . . . . . . . 9 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) → (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
120	119	ralrimiva 3133	. . . . . . . 8 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑦 ∈ 𝐴 (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
121		eqid 2741	. . . . . . . . . 10 ⊢ 𝑋 = 𝑋
122		eqneqall 2947	. . . . . . . . . 10 ⊢ (𝑋 = 𝑋 → (𝑋 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋)))
123	121, 122	ax-mp 5	. . . . . . . . 9 ⊢ (𝑋 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))
124		neeq2 2999	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑋 → (𝑋 ≠ 𝑦 ↔ 𝑋 ≠ 𝑋))
125	98	neeq2d 2996	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑋 → (((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) ↔ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋)))
126	124, 125	imbi12d 346	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑋 → ((𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑋 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
127	126	ralsng 4610	. . . . . . . . . 10 ⊢ (𝑋 ∈ 𝑉 → (∀𝑦 ∈ {𝑋} (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑋 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
128	77, 127	syl 17	. . . . . . . . 9 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (∀𝑦 ∈ {𝑋} (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑋 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
129	123, 128	mpbiri 260	. . . . . . . 8 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑦 ∈ {𝑋} (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
130		ralun 4130	. . . . . . . 8 ⊢ ((∀𝑦 ∈ 𝐴 (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ∧ ∀𝑦 ∈ {𝑋} (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))) → ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
131	120, 129, 130	syl2anc 591	. . . . . . 7 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
132		neeq1 2998	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝑥 ≠ 𝑦 ↔ 𝑋 ≠ 𝑦))
133		fveq2 6831	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) = ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))
134	133	neeq1d 2995	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) ↔ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
135	132, 134	imbi12d 346	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → ((𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
136	135	ralbidv 3164	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
137	136	ralsng 4610	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑉 → (∀𝑥 ∈ {𝑋}∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
138	77, 137	syl 17	. . . . . . 7 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (∀𝑥 ∈ {𝑋}∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
139	131, 138	mpbird 259	. . . . . 6 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑥 ∈ {𝑋}∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
140		ralun 4130	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ∧ ∀𝑥 ∈ {𝑋}∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))) → ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
141	106, 139, 140	syl2anc 591	. . . . 5 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
142	20, 141	jca 517	. . . 4 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}) ∧ ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
143		rnun 6100	. . . . 5 ⊢ ran (𝐺 ∪ {⟨𝑋, 𝑌⟩}) = (ran 𝐺 ∪ ran {⟨𝑋, 𝑌⟩})
144		f1ofo 6778	. . . . . . . 8 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐺:𝐴–onto→𝐵)
145		forn 6746	. . . . . . . 8 ⊢ (𝐺:𝐴–onto→𝐵 → ran 𝐺 = 𝐵)
146	144, 145	syl 17	. . . . . . 7 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → ran 𝐺 = 𝐵)
147	146	3ad2ant1 1140	. . . . . 6 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ran 𝐺 = 𝐵)
148		rnsnopg 6176	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑉 → ran {⟨𝑋, 𝑌⟩} = {𝑌})
149	148	adantr 482	. . . . . . 7 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ran {⟨𝑋, 𝑌⟩} = {𝑌})
150	149	3ad2ant2 1141	. . . . . 6 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ran {⟨𝑋, 𝑌⟩} = {𝑌})
151	147, 150	uneq12d 4102	. . . . 5 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (ran 𝐺 ∪ ran {⟨𝑋, 𝑌⟩}) = (𝐵 ∪ {𝑌}))
152	143, 151	eqtrid 2788	. . . 4 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ran (𝐺 ∪ {⟨𝑋, 𝑌⟩}) = (𝐵 ∪ {𝑌}))
153	142, 152	jca 517	. . 3 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}) ∧ ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))) ∧ ran (𝐺 ∪ {⟨𝑋, 𝑌⟩}) = (𝐵 ∪ {𝑌})))
154		dff1o5 6780	. . . 4 ⊢ ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}) ↔ ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1→(𝐵 ∪ {𝑌}) ∧ ran (𝐺 ∪ {⟨𝑋, 𝑌⟩}) = (𝐵 ∪ {𝑌})))
155		dff14a 7218	. . . 4 ⊢ ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1→(𝐵 ∪ {𝑌}) ↔ ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}) ∧ ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
156	154, 155	bianbi 634	. . 3 ⊢ ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}) ↔ (((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}) ∧ ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))) ∧ ran (𝐺 ∪ {⟨𝑋, 𝑌⟩}) = (𝐵 ∪ {𝑌})))
157	153, 156	sylibr 236	. 2 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}))
158		f1ounsn.f	. . 3 ⊢ 𝐹 = (𝐺 ∪ {⟨𝑋, 𝑌⟩})
159		f1oeq1 6759	. . 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 397 ∨ wo 854 ∧ w3a 1093 = wceq 1548 ∈ wcel 2121 ≠ wne 2936 ∉ wnel 3040 ∀wral 3055 ∪ cun 3883 ⊆ wss 3885 {csn 4558 ⟨cop 4564 dom cdm 5621 ran crn 5622 ⟶wf 6485 –1-1→wf1 6486 –onto→wfo 6487 –1-1-onto→wf1o 6488 ‘cfv 6489

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-10 2154 ax-11 2170 ax-12 2191 ax-ext 2713 ax-sep 5221 ax-nul 5231 ax-pr 5365

This theorem depends on definitions: df-bi 209 df-an 398 df-or 855 df-3an 1095 df-tru 1551 df-fal 1561 df-ex 1788 df-nf 1792 df-sb 2075 df-mo 2545 df-eu 2575 df-clab 2720 df-cleq 2733 df-clel 2816 df-ne 2937 df-nel 3041 df-ral 3056 df-rex 3066 df-rab 3394 df-v 3435 df-dif 3888 df-un 3890 df-in 3892 df-ss 3902 df-nul 4265 df-if 4458 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4842 df-br 5076 df-opab 5138 df-id 5516 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497

This theorem is referenced by: isubgr3stgrlem1 48471

W3C validator