enfixsn - Metamath Proof Explorer

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

Theorem enfixsn 9075

Description: Given two equipollent sets, a bijection can always be chosen which fixes a single point. (Contributed by Stefan O'Rear, 9-Jul-2015.)

**Assertion**
Ref	Expression
enfixsn	⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵))

Distinct variable groups: 𝐴,𝑓 𝐵,𝑓 𝑓,𝑋 𝑓,𝑌

Proof of Theorem enfixsn Dummy variables 𝑔 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp3 1156	. . 3 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) → 𝑋 ≈ 𝑌)
2		bren 8954	. . 3 ⊢ (𝑋 ≈ 𝑌 ↔ ∃𝑔 𝑔:𝑋–1-1-onto→𝑌)
3	1, 2	sylib 221	. 2 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) → ∃𝑔 𝑔:𝑋–1-1-onto→𝑌)
4		relen 8949	. . . . . . . 8 ⊢ Rel ≈
5	4	brrelex2i 5720	. . . . . . 7 ⊢ (𝑋 ≈ 𝑌 → 𝑌 ∈ V)
6	5	3ad2ant3 1153	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) → 𝑌 ∈ V)
7	6	adantr 485	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → 𝑌 ∈ V)
8		f1of 6822	. . . . . . 7 ⊢ (𝑔:𝑋–1-1-onto→𝑌 → 𝑔:𝑋⟶𝑌)
9	8	adantl 486	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → 𝑔:𝑋⟶𝑌)
10		simpl1 1210	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → 𝐴 ∈ 𝑋)
11	9, 10	ffvelcdmd 7082	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → (𝑔‘𝐴) ∈ 𝑌)
12		simpl2 1211	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → 𝐵 ∈ 𝑌)
13		difsnen 9048	. . . . 5 ⊢ ((𝑌 ∈ V ∧ (𝑔‘𝐴) ∈ 𝑌 ∧ 𝐵 ∈ 𝑌) → (𝑌 ∖ {(𝑔‘𝐴)}) ≈ (𝑌 ∖ {𝐵}))
14	7, 11, 12, 13	syl3anc 1398	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → (𝑌 ∖ {(𝑔‘𝐴)}) ≈ (𝑌 ∖ {𝐵}))
15		bren 8954	. . . 4 ⊢ ((𝑌 ∖ {(𝑔‘𝐴)}) ≈ (𝑌 ∖ {𝐵}) ↔ ∃ℎ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
16	14, 15	sylib 221	. . 3 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → ∃ℎ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
17		fvex 6896	. . . . . . . . . . 11 ⊢ (𝑔‘𝐴) ∈ V
18	17	a1i 11	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔‘𝐴) ∈ V)
19		simpl2 1211	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝐵 ∈ 𝑌)
20		f1osng 6865	. . . . . . . . . 10 ⊢ (((𝑔‘𝐴) ∈ V ∧ 𝐵 ∈ 𝑌) → {⟨(𝑔‘𝐴), 𝐵⟩}:{(𝑔‘𝐴)}–1-1-onto→{𝐵})
21	18, 19, 20	syl2anc 595	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → {⟨(𝑔‘𝐴), 𝐵⟩}:{(𝑔‘𝐴)}–1-1-onto→{𝐵})
22		simprr 784	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
23		disjdif 4434	. . . . . . . . . 10 ⊢ ({(𝑔‘𝐴)} ∩ (𝑌 ∖ {(𝑔‘𝐴)})) = ∅
24	23	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({(𝑔‘𝐴)} ∩ (𝑌 ∖ {(𝑔‘𝐴)})) = ∅)
25		disjdif 4434	. . . . . . . . . 10 ⊢ ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅
26	25	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅)
27		f1oun 6842	. . . . . . . . 9 ⊢ ((({⟨(𝑔‘𝐴), 𝐵⟩}:{(𝑔‘𝐴)}–1-1-onto→{𝐵} ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵})) ∧ (({(𝑔‘𝐴)} ∩ (𝑌 ∖ {(𝑔‘𝐴)})) = ∅ ∧ ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅)) → ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})))
28	21, 22, 24, 26, 27	syl22anc 851	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})))
29	8	ad2antrl 740	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔:𝑋⟶𝑌)
30		simpl1 1210	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝐴 ∈ 𝑋)
31	29, 30	ffvelcdmd 7082	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔‘𝐴) ∈ 𝑌)
32		uncom 4113	. . . . . . . . . . 11 ⊢ ({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)})) = ((𝑌 ∖ {(𝑔‘𝐴)}) ∪ {(𝑔‘𝐴)})
33		difsnid 4777	. . . . . . . . . . 11 ⊢ ((𝑔‘𝐴) ∈ 𝑌 → ((𝑌 ∖ {(𝑔‘𝐴)}) ∪ {(𝑔‘𝐴)}) = 𝑌)
34	32, 33	eqtrid 2810	. . . . . . . . . 10 ⊢ ((𝑔‘𝐴) ∈ 𝑌 → ({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)})) = 𝑌)
35	31, 34	syl 18	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)})) = 𝑌)
36		uncom 4113	. . . . . . . . . . 11 ⊢ ({𝐵} ∪ (𝑌 ∖ {𝐵})) = ((𝑌 ∖ {𝐵}) ∪ {𝐵})
37		difsnid 4777	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑌 → ((𝑌 ∖ {𝐵}) ∪ {𝐵}) = 𝑌)
38	36, 37	eqtrid 2810	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝑌 → ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌)
39	19, 38	syl 18	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌)
40		f1oeq23 6813	. . . . . . . . 9 ⊢ ((({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)})) = 𝑌 ∧ ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})) ↔ ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):𝑌–1-1-onto→𝑌))
41	35, 39, 40	syl2anc 595	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})) ↔ ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):𝑌–1-1-onto→𝑌))
42	28, 41	mpbid 235	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):𝑌–1-1-onto→𝑌)
43		simprl 782	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔:𝑋–1-1-onto→𝑌)
44		f1oco 6846	. . . . . . 7 ⊢ ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):𝑌–1-1-onto→𝑌 ∧ 𝑔:𝑋–1-1-onto→𝑌) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌)
45	42, 43, 44	syl2anc 595	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌)
46		f1ofn 6823	. . . . . . . . 9 ⊢ (𝑔:𝑋–1-1-onto→𝑌 → 𝑔 Fn 𝑋)
47	46	ad2antrl 740	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔 Fn 𝑋)
48		fvco2 6980	. . . . . . . 8 ⊢ ((𝑔 Fn 𝑋 ∧ 𝐴 ∈ 𝑋) → ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ)‘(𝑔‘𝐴)))
49	47, 30, 48	syl2anc 595	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ)‘(𝑔‘𝐴)))
50		f1ofn 6823	. . . . . . . . 9 ⊢ ({⟨(𝑔‘𝐴), 𝐵⟩}:{(𝑔‘𝐴)}–1-1-onto→{𝐵} → {⟨(𝑔‘𝐴), 𝐵⟩} Fn {(𝑔‘𝐴)})
51	21, 50	syl 18	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → {⟨(𝑔‘𝐴), 𝐵⟩} Fn {(𝑔‘𝐴)})
52		f1ofn 6823	. . . . . . . . 9 ⊢ (ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → ℎ Fn (𝑌 ∖ {(𝑔‘𝐴)}))
53	52	ad2antll 741	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ℎ Fn (𝑌 ∖ {(𝑔‘𝐴)}))
54	17	snid 4629	. . . . . . . . 9 ⊢ (𝑔‘𝐴) ∈ {(𝑔‘𝐴)}
55	54	a1i 11	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔‘𝐴) ∈ {(𝑔‘𝐴)})
56		fvun1 6974	. . . . . . . 8 ⊢ (({⟨(𝑔‘𝐴), 𝐵⟩} Fn {(𝑔‘𝐴)} ∧ ℎ Fn (𝑌 ∖ {(𝑔‘𝐴)}) ∧ (({(𝑔‘𝐴)} ∩ (𝑌 ∖ {(𝑔‘𝐴)})) = ∅ ∧ (𝑔‘𝐴) ∈ {(𝑔‘𝐴)})) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ)‘(𝑔‘𝐴)) = ({⟨(𝑔‘𝐴), 𝐵⟩}‘(𝑔‘𝐴)))
57	51, 53, 24, 55, 56	syl112anc 1401	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ)‘(𝑔‘𝐴)) = ({⟨(𝑔‘𝐴), 𝐵⟩}‘(𝑔‘𝐴)))
58		fvsng 7180	. . . . . . . 8 ⊢ (((𝑔‘𝐴) ∈ V ∧ 𝐵 ∈ 𝑌) → ({⟨(𝑔‘𝐴), 𝐵⟩}‘(𝑔‘𝐴)) = 𝐵)
59	18, 19, 58	syl2anc 595	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔‘𝐴), 𝐵⟩}‘(𝑔‘𝐴)) = 𝐵)
60	49, 57, 59	3eqtrd 2802	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = 𝐵)
61		snex 5412	. . . . . . . . 9 ⊢ {⟨(𝑔‘𝐴), 𝐵⟩} ∈ V
62		vex 3459	. . . . . . . . 9 ⊢ ℎ ∈ V
63	61, 62	unex 7744	. . . . . . . 8 ⊢ ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∈ V
64		vex 3459	. . . . . . . 8 ⊢ 𝑔 ∈ V
65	63, 64	coex 7928	. . . . . . 7 ⊢ (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔) ∈ V
66		f1oeq1 6810	. . . . . . . 8 ⊢ (𝑓 = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔) → (𝑓:𝑋–1-1-onto→𝑌 ↔ (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌))
67		fveq1 6882	. . . . . . . . 9 ⊢ (𝑓 = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔) → (𝑓‘𝐴) = ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴))
68	67	eqeq1d 2765	. . . . . . . 8 ⊢ (𝑓 = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔) → ((𝑓‘𝐴) = 𝐵 ↔ ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = 𝐵))
69	66, 68	anbi12d 643	. . . . . . 7 ⊢ (𝑓 = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔) → ((𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵) ↔ ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌 ∧ ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = 𝐵)))
70	65, 69	spcev 3566	. . . . . 6 ⊢ (((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌 ∧ ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = 𝐵) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵))
71	45, 60, 70	syl2anc 595	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵))
72	71	expr 461	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → (ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵)))
73	72	exlimdv 1963	. . 3 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → (∃ℎ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵)))
74	16, 73	mpd 16	. 2 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵))
75	3, 74	exlimddv 1965	1 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1103 = wceq 1570 ∃wex 1809 ∈ wcel 2143 Vcvv 3455 ∖ cdif 3903 ∪ cun 3904 ∩ cin 3905 ∅c0 4287 {csn 4590 ⟨cop 4596 class class class wbr 5110 ∘ ccom 5667 Fn wfn 6533 ⟶wf 6534 –1-1-onto→wf1o 6537 ‘cfv 6538 ≈ cen 8941

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-ral 3080 df-rex 3090 df-rab 3417 df-v 3457 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-br 5111 df-opab 5175 df-id 5558 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-en 8945

This theorem is referenced by: mapfien2 9370

W3C validator