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 9147

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 1138	. . 3 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) → 𝑋 ≈ 𝑌)
2		bren 9013	. . 3 ⊢ (𝑋 ≈ 𝑌 ↔ ∃𝑔 𝑔:𝑋–1-1-onto→𝑌)
3	1, 2	sylib 218	. 2 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) → ∃𝑔 𝑔:𝑋–1-1-onto→𝑌)
4		relen 9008	. . . . . . . 8 ⊢ Rel ≈
5	4	brrelex2i 5757	. . . . . . 7 ⊢ (𝑋 ≈ 𝑌 → 𝑌 ∈ V)
6	5	3ad2ant3 1135	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) → 𝑌 ∈ V)
7	6	adantr 480	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → 𝑌 ∈ V)
8		f1of 6862	. . . . . . 7 ⊢ (𝑔:𝑋–1-1-onto→𝑌 → 𝑔:𝑋⟶𝑌)
9	8	adantl 481	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → 𝑔:𝑋⟶𝑌)
10		simpl1 1191	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → 𝐴 ∈ 𝑋)
11	9, 10	ffvelcdmd 7119	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → (𝑔‘𝐴) ∈ 𝑌)
12		simpl2 1192	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → 𝐵 ∈ 𝑌)
13		difsnen 9119	. . . . 5 ⊢ ((𝑌 ∈ V ∧ (𝑔‘𝐴) ∈ 𝑌 ∧ 𝐵 ∈ 𝑌) → (𝑌 ∖ {(𝑔‘𝐴)}) ≈ (𝑌 ∖ {𝐵}))
14	7, 11, 12, 13	syl3anc 1371	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → (𝑌 ∖ {(𝑔‘𝐴)}) ≈ (𝑌 ∖ {𝐵}))
15		bren 9013	. . . 4 ⊢ ((𝑌 ∖ {(𝑔‘𝐴)}) ≈ (𝑌 ∖ {𝐵}) ↔ ∃ℎ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
16	14, 15	sylib 218	. . 3 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → ∃ℎ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
17		fvex 6933	. . . . . . . . . . 11 ⊢ (𝑔‘𝐴) ∈ V
18	17	a1i 11	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔‘𝐴) ∈ V)
19		simpl2 1192	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝐵 ∈ 𝑌)
20		f1osng 6903	. . . . . . . . . 10 ⊢ (((𝑔‘𝐴) ∈ V ∧ 𝐵 ∈ 𝑌) → {⟨(𝑔‘𝐴), 𝐵⟩}:{(𝑔‘𝐴)}–1-1-onto→{𝐵})
21	18, 19, 20	syl2anc 583	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → {⟨(𝑔‘𝐴), 𝐵⟩}:{(𝑔‘𝐴)}–1-1-onto→{𝐵})
22		simprr 772	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
23		disjdif 4495	. . . . . . . . . 10 ⊢ ({(𝑔‘𝐴)} ∩ (𝑌 ∖ {(𝑔‘𝐴)})) = ∅
24	23	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({(𝑔‘𝐴)} ∩ (𝑌 ∖ {(𝑔‘𝐴)})) = ∅)
25		disjdif 4495	. . . . . . . . . 10 ⊢ ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅
26	25	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅)
27		f1oun 6881	. . . . . . . . 9 ⊢ ((({⟨(𝑔‘𝐴), 𝐵⟩}:{(𝑔‘𝐴)}–1-1-onto→{𝐵} ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵})) ∧ (({(𝑔‘𝐴)} ∩ (𝑌 ∖ {(𝑔‘𝐴)})) = ∅ ∧ ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅)) → ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})))
28	21, 22, 24, 26, 27	syl22anc 838	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})))
29	8	ad2antrl 727	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔:𝑋⟶𝑌)
30		simpl1 1191	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝐴 ∈ 𝑋)
31	29, 30	ffvelcdmd 7119	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔‘𝐴) ∈ 𝑌)
32		uncom 4181	. . . . . . . . . . 11 ⊢ ({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)})) = ((𝑌 ∖ {(𝑔‘𝐴)}) ∪ {(𝑔‘𝐴)})
33		difsnid 4835	. . . . . . . . . . 11 ⊢ ((𝑔‘𝐴) ∈ 𝑌 → ((𝑌 ∖ {(𝑔‘𝐴)}) ∪ {(𝑔‘𝐴)}) = 𝑌)
34	32, 33	eqtrid 2792	. . . . . . . . . 10 ⊢ ((𝑔‘𝐴) ∈ 𝑌 → ({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)})) = 𝑌)
35	31, 34	syl 17	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)})) = 𝑌)
36		uncom 4181	. . . . . . . . . . 11 ⊢ ({𝐵} ∪ (𝑌 ∖ {𝐵})) = ((𝑌 ∖ {𝐵}) ∪ {𝐵})
37		difsnid 4835	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑌 → ((𝑌 ∖ {𝐵}) ∪ {𝐵}) = 𝑌)
38	36, 37	eqtrid 2792	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝑌 → ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌)
39	19, 38	syl 17	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌)
40		f1oeq23 6853	. . . . . . . . 9 ⊢ ((({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)})) = 𝑌 ∧ ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})) ↔ ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):𝑌–1-1-onto→𝑌))
41	35, 39, 40	syl2anc 583	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})) ↔ ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):𝑌–1-1-onto→𝑌))
42	28, 41	mpbid 232	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):𝑌–1-1-onto→𝑌)
43		simprl 770	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔:𝑋–1-1-onto→𝑌)
44		f1oco 6885	. . . . . . 7 ⊢ ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ):𝑌–1-1-onto→𝑌 ∧ 𝑔:𝑋–1-1-onto→𝑌) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌)
45	42, 43, 44	syl2anc 583	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌)
46		f1ofn 6863	. . . . . . . . 9 ⊢ (𝑔:𝑋–1-1-onto→𝑌 → 𝑔 Fn 𝑋)
47	46	ad2antrl 727	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔 Fn 𝑋)
48		fvco2 7019	. . . . . . . 8 ⊢ ((𝑔 Fn 𝑋 ∧ 𝐴 ∈ 𝑋) → ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ)‘(𝑔‘𝐴)))
49	47, 30, 48	syl2anc 583	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ)‘(𝑔‘𝐴)))
50		f1ofn 6863	. . . . . . . . 9 ⊢ ({⟨(𝑔‘𝐴), 𝐵⟩}:{(𝑔‘𝐴)}–1-1-onto→{𝐵} → {⟨(𝑔‘𝐴), 𝐵⟩} Fn {(𝑔‘𝐴)})
51	21, 50	syl 17	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → {⟨(𝑔‘𝐴), 𝐵⟩} Fn {(𝑔‘𝐴)})
52		f1ofn 6863	. . . . . . . . 9 ⊢ (ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → ℎ Fn (𝑌 ∖ {(𝑔‘𝐴)}))
53	52	ad2antll 728	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ℎ Fn (𝑌 ∖ {(𝑔‘𝐴)}))
54	17	snid 4684	. . . . . . . . 9 ⊢ (𝑔‘𝐴) ∈ {(𝑔‘𝐴)}
55	54	a1i 11	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔‘𝐴) ∈ {(𝑔‘𝐴)})
56		fvun1 7013	. . . . . . . 8 ⊢ (({⟨(𝑔‘𝐴), 𝐵⟩} Fn {(𝑔‘𝐴)} ∧ ℎ Fn (𝑌 ∖ {(𝑔‘𝐴)}) ∧ (({(𝑔‘𝐴)} ∩ (𝑌 ∖ {(𝑔‘𝐴)})) = ∅ ∧ (𝑔‘𝐴) ∈ {(𝑔‘𝐴)})) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ)‘(𝑔‘𝐴)) = ({⟨(𝑔‘𝐴), 𝐵⟩}‘(𝑔‘𝐴)))
57	51, 53, 24, 55, 56	syl112anc 1374	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ)‘(𝑔‘𝐴)) = ({⟨(𝑔‘𝐴), 𝐵⟩}‘(𝑔‘𝐴)))
58		fvsng 7214	. . . . . . . 8 ⊢ (((𝑔‘𝐴) ∈ V ∧ 𝐵 ∈ 𝑌) → ({⟨(𝑔‘𝐴), 𝐵⟩}‘(𝑔‘𝐴)) = 𝐵)
59	18, 19, 58	syl2anc 583	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔‘𝐴), 𝐵⟩}‘(𝑔‘𝐴)) = 𝐵)
60	49, 57, 59	3eqtrd 2784	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = 𝐵)
61		snex 5451	. . . . . . . . 9 ⊢ {⟨(𝑔‘𝐴), 𝐵⟩} ∈ V
62		vex 3492	. . . . . . . . 9 ⊢ ℎ ∈ V
63	61, 62	unex 7779	. . . . . . . 8 ⊢ ({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∈ V
64		vex 3492	. . . . . . . 8 ⊢ 𝑔 ∈ V
65	63, 64	coex 7970	. . . . . . 7 ⊢ (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔) ∈ V
66		f1oeq1 6850	. . . . . . . 8 ⊢ (𝑓 = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔) → (𝑓:𝑋–1-1-onto→𝑌 ↔ (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌))
67		fveq1 6919	. . . . . . . . 9 ⊢ (𝑓 = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔) → (𝑓‘𝐴) = ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴))
68	67	eqeq1d 2742	. . . . . . . 8 ⊢ (𝑓 = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔) → ((𝑓‘𝐴) = 𝐵 ↔ ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = 𝐵))
69	66, 68	anbi12d 631	. . . . . . 7 ⊢ (𝑓 = (({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔) → ((𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵) ↔ ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌 ∧ ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = 𝐵)))
70	65, 69	spcev 3619	. . . . . 6 ⊢ (((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌 ∧ ((({⟨(𝑔‘𝐴), 𝐵⟩} ∪ ℎ) ∘ 𝑔)‘𝐴) = 𝐵) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵))
71	45, 60, 70	syl2anc 583	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵))
72	71	expr 456	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → (ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵)))
73	72	exlimdv 1932	. . 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 1934	1 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1537 ∃wex 1777 ∈ wcel 2108 Vcvv 3488 ∖ cdif 3973 ∪ cun 3974 ∩ cin 3975 ∅c0 4352 {csn 4648 ⟨cop 4654 class class class wbr 5166 ∘ ccom 5704 Fn wfn 6568 ⟶wf 6569 –1-1-onto→wf1o 6572 ‘cfv 6573 ≈ cen 9000

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-ral 3068 df-rex 3077 df-rab 3444 df-v 3490 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-br 5167 df-opab 5229 df-id 5593 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-en 9004

This theorem is referenced by: mapfien2 9478

W3C validator