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 8629

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 1134	. . 3 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) → 𝑋 ≈ 𝑌)
2		bren 8521	. . 3 ⊢ (𝑋 ≈ 𝑌 ↔ ∃𝑔 𝑔:𝑋–1-1-onto→𝑌)
3	1, 2	sylib 220	. 2 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) → ∃𝑔 𝑔:𝑋–1-1-onto→𝑌)
4		relen 8517	. . . . . . . 8 ⊢ Rel ≈
5	4	brrelex2i 5612	. . . . . . 7 ⊢ (𝑋 ≈ 𝑌 → 𝑌 ∈ V)
6	5	3ad2ant3 1131	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) → 𝑌 ∈ V)
7	6	adantr 483	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → 𝑌 ∈ V)
8		f1of 6618	. . . . . . 7 ⊢ (𝑔:𝑋–1-1-onto→𝑌 → 𝑔:𝑋⟶𝑌)
9	8	adantl 484	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → 𝑔:𝑋⟶𝑌)
10		simpl1 1187	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → 𝐴 ∈ 𝑋)
11	9, 10	ffvelrnd 6855	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → (𝑔‘𝐴) ∈ 𝑌)
12		simpl2 1188	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → 𝐵 ∈ 𝑌)
13		difsnen 8602	. . . . 5 ⊢ ((𝑌 ∈ V ∧ (𝑔‘𝐴) ∈ 𝑌 ∧ 𝐵 ∈ 𝑌) → (𝑌 ∖ {(𝑔‘𝐴)}) ≈ (𝑌 ∖ {𝐵}))
14	7, 11, 12, 13	syl3anc 1367	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → (𝑌 ∖ {(𝑔‘𝐴)}) ≈ (𝑌 ∖ {𝐵}))
15		bren 8521	. . . 4 ⊢ ((𝑌 ∖ {(𝑔‘𝐴)}) ≈ (𝑌 ∖ {𝐵}) ↔ ∃ℎ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
16	14, 15	sylib 220	. . 3 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → ∃ℎ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
17		fvex 6686	. . . . . . . . . . 11 ⊢ (𝑔‘𝐴) ∈ V
18	17	a1i 11	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔‘𝐴) ∈ V)
19		simpl2 1188	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝐵 ∈ 𝑌)
20		f1osng 6658	. . . . . . . . . 10 ⊢ (((𝑔‘𝐴) ∈ V ∧ 𝐵 ∈ 𝑌) → {⟨(𝑔‘𝐴), 𝐵⟩}:{(𝑔‘𝐴)}–1-1-onto→{𝐵})
21	18, 19, 20	syl2anc 586	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → {⟨(𝑔‘𝐴), 𝐵⟩}:{(𝑔‘𝐴)}–1-1-onto→{𝐵})
22		simprr 771	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
23		disjdif 4424	. . . . . . . . . 10 ⊢ ({(𝑔‘𝐴)} ∩ (𝑌 ∖ {(𝑔‘𝐴)})) = ∅
24	23	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({(𝑔‘𝐴)} ∩ (𝑌 ∖ {(𝑔‘𝐴)})) = ∅)
25		disjdif 4424	. . . . . . . . . 10 ⊢ ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅
26	25	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅)
27		f1oun 6637	. . . . . . . . 9 ⊢ ((({⟨(𝑔‘𝐴), 𝐵⟩}:{(𝑔‘𝐴)}–1-1-onto→{𝐵} ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵})) ∧ (({(𝑔‘𝐴)} ∩ (𝑌 ∖ {(𝑔‘𝐴)})) = ∅ ∧ ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅)) → ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})))
28	21, 22, 24, 26, 27	syl22anc 836	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})))
29	8	ad2antrl 726	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔:𝑋⟶𝑌)
30		simpl1 1187	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝐴 ∈ 𝑋)
31	29, 30	ffvelrnd 6855	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔‘𝐴) ∈ 𝑌)
32		uncom 4132	. . . . . . . . . . 11 ⊢ ({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)})) = ((𝑌 ∖ {(𝑔‘𝐴)}) ∪ {(𝑔‘𝐴)})
33		difsnid 4746	. . . . . . . . . . 11 ⊢ ((𝑔‘𝐴) ∈ 𝑌 → ((𝑌 ∖ {(𝑔‘𝐴)}) ∪ {(𝑔‘𝐴)}) = 𝑌)
34	32, 33	syl5eq 2871	. . . . . . . . . 10 ⊢ ((𝑔‘𝐴) ∈ 𝑌 → ({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)})) = 𝑌)
35	31, 34	syl 17	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)})) = 𝑌)
36		uncom 4132	. . . . . . . . . . 11 ⊢ ({𝐵} ∪ (𝑌 ∖ {𝐵})) = ((𝑌 ∖ {𝐵}) ∪ {𝐵})
37		difsnid 4746	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑌 → ((𝑌 ∖ {𝐵}) ∪ {𝐵}) = 𝑌)
38	36, 37	syl5eq 2871	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝑌 → ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌)
39	19, 38	syl 17	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌)
40		f1oeq23 6610	. . . . . . . . 9 ⊢ ((({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)})) = 𝑌 ∧ ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})) ↔ ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):𝑌–1-1-onto→𝑌))
41	35, 39, 40	syl2anc 586	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})) ↔ ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):𝑌–1-1-onto→𝑌))
42	28, 41	mpbid 234	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):𝑌–1-1-onto→𝑌)
43		simprl 769	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔:𝑋–1-1-onto→𝑌)
44		f1oco 6640	. . . . . . 7 ⊢ ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):𝑌–1-1-onto→𝑌 ∧ 𝑔:𝑋–1-1-onto→𝑌) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌)
45	42, 43, 44	syl2anc 586	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌)
46		f1ofn 6619	. . . . . . . . 9 ⊢ (𝑔:𝑋–1-1-onto→𝑌 → 𝑔 Fn 𝑋)
47	46	ad2antrl 726	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔 Fn 𝑋)
48		fvco2 6761	. . . . . . . 8 ⊢ ((𝑔 Fn 𝑋 ∧ 𝐴 ∈ 𝑋) → ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ)‘(𝑔‘𝐴)))
49	47, 30, 48	syl2anc 586	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ)‘(𝑔‘𝐴)))
50		f1ofn 6619	. . . . . . . . 9 ⊢ ({⟨(𝑔‘𝐴), 𝐵⟩}:{(𝑔‘𝐴)}–1-1-onto→{𝐵} → {⟨(𝑔‘𝐴), 𝐵⟩} Fn {(𝑔‘𝐴)})
51	21, 50	syl 17	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → {⟨(𝑔‘𝐴), 𝐵⟩} Fn {(𝑔‘𝐴)})
52		f1ofn 6619	. . . . . . . . 9 ⊢ (ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → ℎ Fn (𝑌 ∖ {(𝑔‘𝐴)}))
53	52	ad2antll 727	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ℎ Fn (𝑌 ∖ {(𝑔‘𝐴)}))
54	17	snid 4604	. . . . . . . . 9 ⊢ (𝑔‘𝐴) ∈ {(𝑔‘𝐴)}
55	54	a1i 11	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔‘𝐴) ∈ {(𝑔‘𝐴)})
56		fvun1 6757	. . . . . . . 8 ⊢ (({⟨(𝑔‘𝐴), 𝐵⟩} Fn {(𝑔‘𝐴)} ∧ ℎ Fn (𝑌 ∖ {(𝑔‘𝐴)}) ∧ (({(𝑔‘𝐴)} ∩ (𝑌 ∖ {(𝑔‘𝐴)})) = ∅ ∧ (𝑔‘𝐴) ∈ {(𝑔‘𝐴)})) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ)‘(𝑔‘𝐴)) = ({⟨(𝑔‘𝐴), 𝐵⟩}‘(𝑔‘𝐴)))
57	51, 53, 24, 55, 56	syl112anc 1370	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ)‘(𝑔‘𝐴)) = ({⟨(𝑔‘𝐴), 𝐵⟩}‘(𝑔‘𝐴)))
58		fvsng 6945	. . . . . . . 8 ⊢ (((𝑔‘𝐴) ∈ V ∧ 𝐵 ∈ 𝑌) → ({⟨(𝑔‘𝐴), 𝐵⟩}‘(𝑔‘𝐴)) = 𝐵)
59	18, 19, 58	syl2anc 586	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔‘𝐴), 𝐵⟩}‘(𝑔‘𝐴)) = 𝐵)
60	49, 57, 59	3eqtrd 2863	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = 𝐵)
61		snex 5335	. . . . . . . . 9 ⊢ {⟨(𝑔‘𝐴), 𝐵⟩} ∈ V
62		vex 3500	. . . . . . . . 9 ⊢ ℎ ∈ V
63	61, 62	unex 7472	. . . . . . . 8 ⊢ ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∈ V
64		vex 3500	. . . . . . . 8 ⊢ 𝑔 ∈ V
65	63, 64	coex 7638	. . . . . . 7 ⊢ (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔) ∈ V
66		f1oeq1 6607	. . . . . . . 8 ⊢ (𝑓 = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔) → (𝑓:𝑋–1-1-onto→𝑌 ↔ (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌))
67		fveq1 6672	. . . . . . . . 9 ⊢ (𝑓 = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔) → (𝑓‘𝐴) = ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴))
68	67	eqeq1d 2826	. . . . . . . 8 ⊢ (𝑓 = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔) → ((𝑓‘𝐴) = 𝐵 ↔ ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = 𝐵))
69	66, 68	anbi12d 632	. . . . . . 7 ⊢ (𝑓 = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔) → ((𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵) ↔ ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌 ∧ ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = 𝐵)))
70	65, 69	spcev 3610	. . . . . 6 ⊢ (((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌 ∧ ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = 𝐵) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵))
71	45, 60, 70	syl2anc 586	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵))
72	71	expr 459	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → (ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵)))
73	72	exlimdv 1933	. . 3 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → (∃ℎ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵)))
74	16, 73	mpd 15	. 2 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵))
75	3, 74	exlimddv 1935	1 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1536 ∃wex 1779 ∈ wcel 2113 Vcvv 3497 ∖ cdif 3936 ∪ cun 3937 ∩ cin 3938 ∅c0 4294 {csn 4570 ⟨cop 4576 class class class wbr 5069 ∘ ccom 5562 Fn wfn 6353 ⟶wf 6354 –1-1-onto→wf1o 6357 ‘cfv 6358 ≈ cen 8509

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 ax-sep 5206 ax-nul 5213 ax-pow 5269 ax-pr 5333 ax-un 7464

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-mo 2621 df-eu 2653 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-ne 3020 df-ral 3146 df-rex 3147 df-rab 3150 df-v 3499 df-sbc 3776 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-nul 4295 df-if 4471 df-pw 4544 df-sn 4571 df-pr 4573 df-op 4577 df-uni 4842 df-br 5070 df-opab 5132 df-id 5463 df-xp 5564 df-rel 5565 df-cnv 5566 df-co 5567 df-dm 5568 df-rn 5569 df-res 5570 df-ima 5571 df-suc 6200 df-iota 6317 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365 df-fv 6366 df-1o 8105 df-er 8292 df-en 8513

This theorem is referenced by: mapfien2 8875

W3C validator