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 7271

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 6821	. . . . . . . . 9 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐺:𝐴⟶𝐵)
2		ssun1 4139	. . . . . . . . . 10 ⊢ 𝐵 ⊆ (𝐵 ∪ {𝑌})
3	2	a1i 11	. . . . . . . . 9 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐵 ⊆ (𝐵 ∪ {𝑌}))
4	1, 3	fssd 6724	. . . . . . . 8 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐺:𝐴⟶(𝐵 ∪ {𝑌}))
5	4	3ad2ant1 1149	. . . . . . 7 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝐺:𝐴⟶(𝐵 ∪ {𝑌}))
6		simpl 487	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → 𝑋 ∈ 𝑉)
7		df-nel 3071	. . . . . . . . . . 11 ⊢ (𝑋 ∉ 𝐴 ↔ ¬ 𝑋 ∈ 𝐴)
8	7	biimpi 219	. . . . . . . . . 10 ⊢ (𝑋 ∉ 𝐴 → ¬ 𝑋 ∈ 𝐴)
9	8	adantr 485	. . . . . . . . 9 ⊢ ((𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵) → ¬ 𝑋 ∈ 𝐴)
10	6, 9	anim12i 624	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝐴))
11	10	3adant1 1146	. . . . . . 7 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝐴))
12		eqid 2769	. . . . . . . . . . 11 ⊢ 𝑌 = 𝑌
13	12	olci 879	. . . . . . . . . 10 ⊢ (𝑌 ∈ 𝐵 ∨ 𝑌 = 𝑌)
14		elunsn 4654	. . . . . . . . . 10 ⊢ (𝑌 ∈ 𝑊 → (𝑌 ∈ (𝐵 ∪ {𝑌}) ↔ (𝑌 ∈ 𝐵 ∨ 𝑌 = 𝑌)))
15	13, 14	mpbiri 261	. . . . . . . . 9 ⊢ (𝑌 ∈ 𝑊 → 𝑌 ∈ (𝐵 ∪ {𝑌}))
16	15	adantl 486	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → 𝑌 ∈ (𝐵 ∪ {𝑌}))
17	16	3ad2ant2 1150	. . . . . . 7 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝑌 ∈ (𝐵 ∪ {𝑌}))
18	5, 11, 17	3jca 1144	. . . . . 6 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝐺:𝐴⟶(𝐵 ∪ {𝑌}) ∧ (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝐴) ∧ 𝑌 ∈ (𝐵 ∪ {𝑌})))
19		fsnunf 7184	. . . . . 6 ⊢ ((𝐺:𝐴⟶(𝐵 ∪ {𝑌}) ∧ (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝐴) ∧ 𝑌 ∈ (𝐵 ∪ {𝑌})) → (𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}))
20	18, 19	syl 18	. . . . 5 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}))
21		f1of1 6820	. . . . . . . . . . . . . . 15 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐺:𝐴–1-1→𝐵)
22		dff14a 7269	. . . . . . . . . . . . . . . 16 ⊢ (𝐺:𝐴–1-1→𝐵 ↔ (𝐺:𝐴⟶𝐵 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎 ≠ 𝑏 → (𝐺‘𝑎) ≠ (𝐺‘𝑏))))
23		neeq1 3026	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑥 → (𝑎 ≠ 𝑏 ↔ 𝑥 ≠ 𝑏))
24		fveq2 6882	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑥 → (𝐺‘𝑎) = (𝐺‘𝑥))
25	24	neeq1d 3023	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑥 → ((𝐺‘𝑎) ≠ (𝐺‘𝑏) ↔ (𝐺‘𝑥) ≠ (𝐺‘𝑏)))
26	23, 25	imbi12d 347	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑥 → ((𝑎 ≠ 𝑏 → (𝐺‘𝑎) ≠ (𝐺‘𝑏)) ↔ (𝑥 ≠ 𝑏 → (𝐺‘𝑥) ≠ (𝐺‘𝑏))))
27		neeq2 3027	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = 𝑦 → (𝑥 ≠ 𝑏 ↔ 𝑥 ≠ 𝑦))
28		fveq2 6882	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = 𝑦 → (𝐺‘𝑏) = (𝐺‘𝑦))
29	28	neeq2d 3024	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = 𝑦 → ((𝐺‘𝑥) ≠ (𝐺‘𝑏) ↔ (𝐺‘𝑥) ≠ (𝐺‘𝑦)))
30	27, 29	imbi12d 347	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 𝑦 → ((𝑥 ≠ 𝑏 → (𝐺‘𝑥) ≠ (𝐺‘𝑏)) ↔ (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
31	26, 30	rspc2va 3602	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎 ≠ 𝑏 → (𝐺‘𝑎) ≠ (𝐺‘𝑏))) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)))
32	31	expcom 418	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎 ≠ 𝑏 → (𝐺‘𝑎) ≠ (𝐺‘𝑏)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
33	32	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺:𝐴⟶𝐵 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎 ≠ 𝑏 → (𝐺‘𝑎) ≠ (𝐺‘𝑏))) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
34	22, 33	sylbi 220	. . . . . . . . . . . . . . 15 ⊢ (𝐺:𝐴–1-1→𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
35	21, 34	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
36	35	3ad2ant1 1149	. . . . . . . . . . . . 13 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
37	36	impl 460	. . . . . . . . . . . 12 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)))
38	37	imp 411	. . . . . . . . . . 11 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → (𝐺‘𝑥) ≠ (𝐺‘𝑦))
39		nelne2 3062	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑥 ≠ 𝑋)
40	39	necomd 3019	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑋 ≠ 𝑥)
41	40	expcom 418	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑋 ∈ 𝐴 → (𝑥 ∈ 𝐴 → 𝑋 ≠ 𝑥))
42	7, 41	sylbi 220	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∉ 𝐴 → (𝑥 ∈ 𝐴 → 𝑋 ≠ 𝑥))
43	42	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵) → (𝑥 ∈ 𝐴 → 𝑋 ≠ 𝑥))
44	43	3ad2ant3 1151	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝑥 ∈ 𝐴 → 𝑋 ≠ 𝑥))
45	44	imp 411	. . . . . . . . . . . . . 14 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑋 ≠ 𝑥)
46	45	adantr 485	. . . . . . . . . . . . 13 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑋 ≠ 𝑥)
47	46	adantr 485	. . . . . . . . . . . 12 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → 𝑋 ≠ 𝑥)
48		fvunsn 7178	. . . . . . . . . . . 12 ⊢ (𝑋 ≠ 𝑥 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) = (𝐺‘𝑥))
49	47, 48	syl 18	. . . . . . . . . . 11 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) = (𝐺‘𝑥))
50		nelne2 3062	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑦 ≠ 𝑋)
51	50	necomd 3019	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑋 ≠ 𝑦)
52	51	expcom 418	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑋 ∈ 𝐴 → (𝑦 ∈ 𝐴 → 𝑋 ≠ 𝑦))
53	7, 52	sylbi 220	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∉ 𝐴 → (𝑦 ∈ 𝐴 → 𝑋 ≠ 𝑦))
54	53	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵) → (𝑦 ∈ 𝐴 → 𝑋 ≠ 𝑦))
55	54	3ad2ant3 1151	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝑦 ∈ 𝐴 → 𝑋 ≠ 𝑦))
56	55	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐴 → 𝑋 ≠ 𝑦))
57	56	imp 411	. . . . . . . . . . . . 13 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑋 ≠ 𝑦)
58	57	adantr 485	. . . . . . . . . . . 12 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → 𝑋 ≠ 𝑦)
59		fvunsn 7178	. . . . . . . . . . . 12 ⊢ (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) = (𝐺‘𝑦))
60	58, 59	syl 18	. . . . . . . . . . 11 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) = (𝐺‘𝑦))
61	38, 49, 60	3netr4d 3041	. . . . . . . . . 10 ⊢ (((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))
62	61	ex 417	. . . . . . . . 9 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
63	62	ralrimiva 3163	. . . . . . . 8 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
64	1	3ad2ant1 1149	. . . . . . . . . . . . . 14 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝐺:𝐴⟶𝐵)
65	64	ffvelcdmda 7080	. . . . . . . . . . . . 13 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ 𝐵)
66		df-nel 3071	. . . . . . . . . . . . . . . . 17 ⊢ (𝑌 ∉ 𝐵 ↔ ¬ 𝑌 ∈ 𝐵)
67	66	biimpi 219	. . . . . . . . . . . . . . . 16 ⊢ (𝑌 ∉ 𝐵 → ¬ 𝑌 ∈ 𝐵)
68	67	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵) → ¬ 𝑌 ∈ 𝐵)
69	68	3ad2ant3 1151	. . . . . . . . . . . . . 14 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ¬ 𝑌 ∈ 𝐵)
70	69	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → ¬ 𝑌 ∈ 𝐵)
71		nelne2 3062	. . . . . . . . . . . . 13 ⊢ (((𝐺‘𝑥) ∈ 𝐵 ∧ ¬ 𝑌 ∈ 𝐵) → (𝐺‘𝑥) ≠ 𝑌)
72	65, 70, 71	syl2anc 595	. . . . . . . . . . . 12 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ≠ 𝑌)
73	72	adantr 485	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → (𝐺‘𝑥) ≠ 𝑌)
74		simpr 489	. . . . . . . . . . . . 13 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → 𝑥 ≠ 𝑋)
75	74	necomd 3019	. . . . . . . . . . . 12 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → 𝑋 ≠ 𝑥)
76	75, 48	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) = (𝐺‘𝑥))
77	6	3ad2ant2 1150	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝑋 ∈ 𝑉)
78		simpr 489	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → 𝑌 ∈ 𝑊)
79	78	3ad2ant2 1150	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝑌 ∈ 𝑊)
80		f1odm 6825	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → dom 𝐺 = 𝐴)
81	80	eqcomd 2775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐴 = dom 𝐺)
82	81	eleq2d 2855	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → (𝑋 ∈ 𝐴 ↔ 𝑋 ∈ dom 𝐺))
83	82	notbid 321	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → (¬ 𝑋 ∈ 𝐴 ↔ ¬ 𝑋 ∈ dom 𝐺))
84	7, 83	bitrid 286	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → (𝑋 ∉ 𝐴 ↔ ¬ 𝑋 ∈ dom 𝐺))
85	84	biimpd 232	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → (𝑋 ∉ 𝐴 → ¬ 𝑋 ∈ dom 𝐺))
86	85	adantrd 496	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → ((𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵) → ¬ 𝑋 ∈ dom 𝐺))
87	86	imp 411	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ¬ 𝑋 ∈ dom 𝐺)
88	87	3adant2 1147	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ¬ 𝑋 ∈ dom 𝐺)
89	77, 79, 88	3jca 1144	. . . . . . . . . . . . . 14 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺))
90	89	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺))
91	90	adantr 485	. . . . . . . . . . . 12 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺))
92		fsnunfv 7186	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) = 𝑌)
93	91, 92	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) = 𝑌)
94	73, 76, 93	3netr4d 3041	. . . . . . . . . 10 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 𝑋) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))
95	94	ex 417	. . . . . . . . 9 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝑥 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋)))
96	77	adantr 485	. . . . . . . . . 10 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑋 ∈ 𝑉)
97		neeq2 3027	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑋 → (𝑥 ≠ 𝑦 ↔ 𝑥 ≠ 𝑋))
98		fveq2 6882	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) = ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))
99	98	neeq2d 3024	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑋 → (((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) ↔ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋)))
100	97, 99	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑋 → ((𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑥 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
101	100	ralsng 4646	. . . . . . . . . 10 ⊢ (𝑋 ∈ 𝑉 → (∀𝑦 ∈ {𝑋} (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑥 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
102	96, 101	syl 18	. . . . . . . . 9 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ {𝑋} (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑥 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
103	95, 102	mpbird 260	. . . . . . . 8 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ {𝑋} (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
104		ralun 4159	. . . . . . . 8 ⊢ ((∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ∧ ∀𝑦 ∈ {𝑋} (𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))) → ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
105	63, 103, 104	syl2anc 595	. . . . . . 7 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
106	105	ralrimiva 3163	. . . . . 6 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
107	64	ffvelcdmda 7080	. . . . . . . . . . . . . 14 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) → (𝐺‘𝑦) ∈ 𝐵)
108	69	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) → ¬ 𝑌 ∈ 𝐵)
109	107, 108	jca 520	. . . . . . . . . . . . 13 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) → ((𝐺‘𝑦) ∈ 𝐵 ∧ ¬ 𝑌 ∈ 𝐵))
110	109	adantr 485	. . . . . . . . . . . 12 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → ((𝐺‘𝑦) ∈ 𝐵 ∧ ¬ 𝑌 ∈ 𝐵))
111		nelne2 3062	. . . . . . . . . . . . 13 ⊢ (((𝐺‘𝑦) ∈ 𝐵 ∧ ¬ 𝑌 ∈ 𝐵) → (𝐺‘𝑦) ≠ 𝑌)
112	111	necomd 3019	. . . . . . . . . . . 12 ⊢ (((𝐺‘𝑦) ∈ 𝐵 ∧ ¬ 𝑌 ∈ 𝐵) → 𝑌 ≠ (𝐺‘𝑦))
113	110, 112	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → 𝑌 ≠ (𝐺‘𝑦))
114	89	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺))
115	114	adantr 485	. . . . . . . . . . . 12 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐺))
116	115, 92	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) = 𝑌)
117	59	adantl 486	. . . . . . . . . . 11 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) = (𝐺‘𝑦))
118	113, 116, 117	3netr4d 3041	. . . . . . . . . 10 ⊢ ((((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ≠ 𝑦) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))
119	118	ex 417	. . . . . . . . 9 ⊢ (((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) ∧ 𝑦 ∈ 𝐴) → (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
120	119	ralrimiva 3163	. . . . . . . 8 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑦 ∈ 𝐴 (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
121		eqid 2769	. . . . . . . . . 10 ⊢ 𝑋 = 𝑋
122		eqneqall 2975	. . . . . . . . . 10 ⊢ (𝑋 = 𝑋 → (𝑋 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋)))
123	121, 122	ax-mp 5	. . . . . . . . 9 ⊢ (𝑋 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))
124		neeq2 3027	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑋 → (𝑋 ≠ 𝑦 ↔ 𝑋 ≠ 𝑋))
125	98	neeq2d 3024	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑋 → (((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) ↔ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋)))
126	124, 125	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑋 → ((𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑋 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
127	126	ralsng 4646	. . . . . . . . . 10 ⊢ (𝑋 ∈ 𝑉 → (∀𝑦 ∈ {𝑋} (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑋 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
128	77, 127	syl 18	. . . . . . . . 9 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (∀𝑦 ∈ {𝑋} (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑋 ≠ 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))))
129	123, 128	mpbiri 261	. . . . . . . 8 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑦 ∈ {𝑋} (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
130		ralun 4159	. . . . . . . 8 ⊢ ((∀𝑦 ∈ 𝐴 (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ∧ ∀𝑦 ∈ {𝑋} (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))) → ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
131	120, 129, 130	syl2anc 595	. . . . . . 7 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
132		neeq1 3026	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝑥 ≠ 𝑦 ↔ 𝑋 ≠ 𝑦))
133		fveq2 6882	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) = ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))
134	133	neeq1d 3023	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦) ↔ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
135	132, 134	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → ((𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ (𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
136	135	ralbidv 3194	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
137	136	ralsng 4646	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑉 → (∀𝑥 ∈ {𝑋}∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
138	77, 137	syl 18	. . . . . . 7 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (∀𝑥 ∈ {𝑋}∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ↔ ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑋 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
139	131, 138	mpbird 260	. . . . . 6 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑥 ∈ {𝑋}∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
140		ralun 4159	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)) ∧ ∀𝑥 ∈ {𝑋}∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))) → ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
141	106, 139, 140	syl2anc 595	. . . . 5 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦)))
142	20, 141	jca 520	. . . 4 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}) ∧ ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
143		rnun 6143	. . . . 5 ⊢ ran (𝐺 ∪ {⟨𝑋, 𝑌⟩}) = (ran 𝐺 ∪ ran {⟨𝑋, 𝑌⟩})
144		f1ofo 6829	. . . . . . . 8 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → 𝐺:𝐴–onto→𝐵)
145		forn 6796	. . . . . . . 8 ⊢ (𝐺:𝐴–onto→𝐵 → ran 𝐺 = 𝐵)
146	144, 145	syl 18	. . . . . . 7 ⊢ (𝐺:𝐴–1-1-onto→𝐵 → ran 𝐺 = 𝐵)
147	146	3ad2ant1 1149	. . . . . 6 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ran 𝐺 = 𝐵)
148		rnsnopg 6223	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑉 → ran {⟨𝑋, 𝑌⟩} = {𝑌})
149	148	adantr 485	. . . . . . 7 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ran {⟨𝑋, 𝑌⟩} = {𝑌})
150	149	3ad2ant2 1150	. . . . . 6 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ran {⟨𝑋, 𝑌⟩} = {𝑌})
151	147, 150	uneq12d 4131	. . . . 5 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (ran 𝐺 ∪ ran {⟨𝑋, 𝑌⟩}) = (𝐵 ∪ {𝑌}))
152	143, 151	eqtrid 2816	. . . 4 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → ran (𝐺 ∪ {⟨𝑋, 𝑌⟩}) = (𝐵 ∪ {𝑌}))
153	142, 152	jca 520	. . 3 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}) ∧ ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))) ∧ ran (𝐺 ∪ {⟨𝑋, 𝑌⟩}) = (𝐵 ∪ {𝑌})))
154		dff1o5 6831	. . . 4 ⊢ ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}) ↔ ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1→(𝐵 ∪ {𝑌}) ∧ ran (𝐺 ∪ {⟨𝑋, 𝑌⟩}) = (𝐵 ∪ {𝑌})))
155		dff14a 7269	. . . 4 ⊢ ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1→(𝐵 ∪ {𝑌}) ↔ ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}) ∧ ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))))
156	154, 155	bianbi 638	. . 3 ⊢ ((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}) ↔ (((𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})⟶(𝐵 ∪ {𝑌}) ∧ ∀𝑥 ∈ (𝐴 ∪ {𝑋})∀𝑦 ∈ (𝐴 ∪ {𝑋})(𝑥 ≠ 𝑦 → ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑥) ≠ ((𝐺 ∪ {⟨𝑋, 𝑌⟩})‘𝑦))) ∧ ran (𝐺 ∪ {⟨𝑋, 𝑌⟩}) = (𝐵 ∪ {𝑌})))
157	153, 156	sylibr 237	. 2 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → (𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}))
158		f1ounsn.f	. . 3 ⊢ 𝐹 = (𝐺 ∪ {⟨𝑋, 𝑌⟩})
159		f1oeq1 6809	. . 3 ⊢ (𝐹 = (𝐺 ∪ {⟨𝑋, 𝑌⟩}) → (𝐹:(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}) ↔ (𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌})))
160	158, 159	ax-mp 5	. 2 ⊢ (𝐹:(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}) ↔ (𝐺 ∪ {⟨𝑋, 𝑌⟩}):(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}))
161	157, 160	sylibr 237	1 ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝐹:(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∧ w3a 1101 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 ∉ wnel 3070 ∀wral 3085 ∪ cun 3911 ⊆ wss 3913 {csn 4594 ⟨cop 4600 dom cdm 5662 ran crn 5663 ⟶wf 6533 –1-1→wf1 6534 –onto→wfo 6535 –1-1-onto→wf1o 6536 ‘cfv 6537

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5261 ax-nul 5271 ax-pr 5405

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rab 3424 df-v 3465 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4493 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-br 5114 df-opab 5178 df-id 5557 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545

This theorem is referenced by: isubgr3stgrlem1 48654

W3C validator