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 8422

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 1118	. . 3 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) → 𝑋 ≈ 𝑌)
2		bren 8315	. . 3 ⊢ (𝑋 ≈ 𝑌 ↔ ∃𝑔 𝑔:𝑋–1-1-onto→𝑌)
3	1, 2	sylib 210	. 2 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) → ∃𝑔 𝑔:𝑋–1-1-onto→𝑌)
4		relen 8311	. . . . . . . 8 ⊢ Rel ≈
5	4	brrelex2i 5459	. . . . . . 7 ⊢ (𝑋 ≈ 𝑌 → 𝑌 ∈ V)
6	5	3ad2ant3 1115	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) → 𝑌 ∈ V)
7	6	adantr 473	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → 𝑌 ∈ V)
8		f1of 6444	. . . . . . 7 ⊢ (𝑔:𝑋–1-1-onto→𝑌 → 𝑔:𝑋⟶𝑌)
9	8	adantl 474	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → 𝑔:𝑋⟶𝑌)
10		simpl1 1171	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → 𝐴 ∈ 𝑋)
11	9, 10	ffvelrnd 6677	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → (𝑔‘𝐴) ∈ 𝑌)
12		simpl2 1172	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → 𝐵 ∈ 𝑌)
13		difsnen 8395	. . . . 5 ⊢ ((𝑌 ∈ V ∧ (𝑔‘𝐴) ∈ 𝑌 ∧ 𝐵 ∈ 𝑌) → (𝑌 ∖ {(𝑔‘𝐴)}) ≈ (𝑌 ∖ {𝐵}))
14	7, 11, 12, 13	syl3anc 1351	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → (𝑌 ∖ {(𝑔‘𝐴)}) ≈ (𝑌 ∖ {𝐵}))
15		bren 8315	. . . 4 ⊢ ((𝑌 ∖ {(𝑔‘𝐴)}) ≈ (𝑌 ∖ {𝐵}) ↔ ∃ℎ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
16	14, 15	sylib 210	. . 3 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → ∃ℎ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
17		fvex 6512	. . . . . . . . . . 11 ⊢ (𝑔‘𝐴) ∈ V
18	17	a1i 11	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔‘𝐴) ∈ V)
19		simpl2 1172	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝐵 ∈ 𝑌)
20		f1osng 6484	. . . . . . . . . 10 ⊢ (((𝑔‘𝐴) ∈ V ∧ 𝐵 ∈ 𝑌) → {⟨(𝑔‘𝐴), 𝐵⟩}:{(𝑔‘𝐴)}–1-1-onto→{𝐵})
21	18, 19, 20	syl2anc 576	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → {⟨(𝑔‘𝐴), 𝐵⟩}:{(𝑔‘𝐴)}–1-1-onto→{𝐵})
22		simprr 760	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
23		disjdif 4304	. . . . . . . . . 10 ⊢ ({(𝑔‘𝐴)} ∩ (𝑌 ∖ {(𝑔‘𝐴)})) = ∅
24	23	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({(𝑔‘𝐴)} ∩ (𝑌 ∖ {(𝑔‘𝐴)})) = ∅)
25		disjdif 4304	. . . . . . . . . 10 ⊢ ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅
26	25	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅)
27		f1oun 6463	. . . . . . . . 9 ⊢ ((({⟨(𝑔‘𝐴), 𝐵⟩}:{(𝑔‘𝐴)}–1-1-onto→{𝐵} ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵})) ∧ (({(𝑔‘𝐴)} ∩ (𝑌 ∖ {(𝑔‘𝐴)})) = ∅ ∧ ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅)) → ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})))
28	21, 22, 24, 26, 27	syl22anc 826	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})))
29	8	ad2antrl 715	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔:𝑋⟶𝑌)
30		simpl1 1171	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝐴 ∈ 𝑋)
31	29, 30	ffvelrnd 6677	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔‘𝐴) ∈ 𝑌)
32		uncom 4018	. . . . . . . . . . 11 ⊢ ({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)})) = ((𝑌 ∖ {(𝑔‘𝐴)}) ∪ {(𝑔‘𝐴)})
33		difsnid 4617	. . . . . . . . . . 11 ⊢ ((𝑔‘𝐴) ∈ 𝑌 → ((𝑌 ∖ {(𝑔‘𝐴)}) ∪ {(𝑔‘𝐴)}) = 𝑌)
34	32, 33	syl5eq 2826	. . . . . . . . . 10 ⊢ ((𝑔‘𝐴) ∈ 𝑌 → ({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)})) = 𝑌)
35	31, 34	syl 17	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)})) = 𝑌)
36		uncom 4018	. . . . . . . . . . 11 ⊢ ({𝐵} ∪ (𝑌 ∖ {𝐵})) = ((𝑌 ∖ {𝐵}) ∪ {𝐵})
37		difsnid 4617	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑌 → ((𝑌 ∖ {𝐵}) ∪ {𝐵}) = 𝑌)
38	36, 37	syl5eq 2826	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝑌 → ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌)
39	19, 38	syl 17	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌)
40		f1oeq23 6436	. . . . . . . . 9 ⊢ ((({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)})) = 𝑌 ∧ ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})) ↔ ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):𝑌–1-1-onto→𝑌))
41	35, 39, 40	syl2anc 576	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})) ↔ ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):𝑌–1-1-onto→𝑌))
42	28, 41	mpbid 224	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):𝑌–1-1-onto→𝑌)
43		simprl 758	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔:𝑋–1-1-onto→𝑌)
44		f1oco 6466	. . . . . . 7 ⊢ ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):𝑌–1-1-onto→𝑌 ∧ 𝑔:𝑋–1-1-onto→𝑌) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌)
45	42, 43, 44	syl2anc 576	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌)
46		f1ofn 6445	. . . . . . . . 9 ⊢ (𝑔:𝑋–1-1-onto→𝑌 → 𝑔 Fn 𝑋)
47	46	ad2antrl 715	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔 Fn 𝑋)
48		fvco2 6586	. . . . . . . 8 ⊢ ((𝑔 Fn 𝑋 ∧ 𝐴 ∈ 𝑋) → ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ)‘(𝑔‘𝐴)))
49	47, 30, 48	syl2anc 576	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ)‘(𝑔‘𝐴)))
50		f1ofn 6445	. . . . . . . . 9 ⊢ ({⟨(𝑔‘𝐴), 𝐵⟩}:{(𝑔‘𝐴)}–1-1-onto→{𝐵} → {⟨(𝑔‘𝐴), 𝐵⟩} Fn {(𝑔‘𝐴)})
51	21, 50	syl 17	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → {⟨(𝑔‘𝐴), 𝐵⟩} Fn {(𝑔‘𝐴)})
52		f1ofn 6445	. . . . . . . . 9 ⊢ (ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → ℎ Fn (𝑌 ∖ {(𝑔‘𝐴)}))
53	52	ad2antll 716	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ℎ Fn (𝑌 ∖ {(𝑔‘𝐴)}))
54	17	snid 4473	. . . . . . . . 9 ⊢ (𝑔‘𝐴) ∈ {(𝑔‘𝐴)}
55	54	a1i 11	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔‘𝐴) ∈ {(𝑔‘𝐴)})
56		fvun1 6582	. . . . . . . 8 ⊢ (({⟨(𝑔‘𝐴), 𝐵⟩} Fn {(𝑔‘𝐴)} ∧ ℎ Fn (𝑌 ∖ {(𝑔‘𝐴)}) ∧ (({(𝑔‘𝐴)} ∩ (𝑌 ∖ {(𝑔‘𝐴)})) = ∅ ∧ (𝑔‘𝐴) ∈ {(𝑔‘𝐴)})) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ)‘(𝑔‘𝐴)) = ({⟨(𝑔‘𝐴), 𝐵⟩}‘(𝑔‘𝐴)))
57	51, 53, 24, 55, 56	syl112anc 1354	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ)‘(𝑔‘𝐴)) = ({⟨(𝑔‘𝐴), 𝐵⟩}‘(𝑔‘𝐴)))
58		fvsng 6765	. . . . . . . 8 ⊢ (((𝑔‘𝐴) ∈ V ∧ 𝐵 ∈ 𝑌) → ({⟨(𝑔‘𝐴), 𝐵⟩}‘(𝑔‘𝐴)) = 𝐵)
59	18, 19, 58	syl2anc 576	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔‘𝐴), 𝐵⟩}‘(𝑔‘𝐴)) = 𝐵)
60	49, 57, 59	3eqtrd 2818	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = 𝐵)
61		snex 5188	. . . . . . . . 9 ⊢ {⟨(𝑔‘𝐴), 𝐵⟩} ∈ V
62		vex 3418	. . . . . . . . 9 ⊢ ℎ ∈ V
63	61, 62	unex 7286	. . . . . . . 8 ⊢ ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∈ V
64		vex 3418	. . . . . . . 8 ⊢ 𝑔 ∈ V
65	63, 64	coex 7450	. . . . . . 7 ⊢ (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔) ∈ V
66		f1oeq1 6433	. . . . . . . 8 ⊢ (𝑓 = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔) → (𝑓:𝑋–1-1-onto→𝑌 ↔ (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌))
67		fveq1 6498	. . . . . . . . 9 ⊢ (𝑓 = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔) → (𝑓‘𝐴) = ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴))
68	67	eqeq1d 2780	. . . . . . . 8 ⊢ (𝑓 = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔) → ((𝑓‘𝐴) = 𝐵 ↔ ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = 𝐵))
69	66, 68	anbi12d 621	. . . . . . 7 ⊢ (𝑓 = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔) → ((𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵) ↔ ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌 ∧ ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = 𝐵)))
70	65, 69	spcev 3525	. . . . . 6 ⊢ (((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌 ∧ ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = 𝐵) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵))
71	45, 60, 70	syl2anc 576	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵))
72	71	expr 449	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → (ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵)))
73	72	exlimdv 1892	. . 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 1894	1 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 ∧ w3a 1068 = wceq 1507 ∃wex 1742 ∈ wcel 2050 Vcvv 3415 ∖ cdif 3826 ∪ cun 3827 ∩ cin 3828 ∅c0 4178 {csn 4441 ⟨cop 4447 class class class wbr 4929 ∘ ccom 5411 Fn wfn 6183 ⟶wf 6184 –1-1-onto→wf1o 6187 ‘cfv 6188 ≈ cen 8303

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5060 ax-nul 5067 ax-pow 5119 ax-pr 5186 ax-un 7279

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-sbc 3682 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-nul 4179 df-if 4351 df-pw 4424 df-sn 4442 df-pr 4444 df-op 4448 df-uni 4713 df-br 4930 df-opab 4992 df-id 5312 df-xp 5413 df-rel 5414 df-cnv 5415 df-co 5416 df-dm 5417 df-rn 5418 df-res 5419 df-ima 5420 df-suc 6035 df-iota 6152 df-fun 6190 df-fn 6191 df-f 6192 df-f1 6193 df-fo 6194 df-f1o 6195 df-fv 6196 df-1o 7905 df-er 8089 df-en 8307

This theorem is referenced by: mapfien2 8667

W3C validator