Theorem phpreu 38366

Description: Theorem related to pigeonhole principle. (Contributed by Brendan Leahy, 21-Aug-2020.)

Assertion

Ref	Expression
phpreu	⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥 = 𝐶))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶

Allowed substitution hint:   𝐶(𝑦)

Proof of Theorem phpreu

Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2850	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝐶 → (𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴))
2	1	biimpac 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐶) → 𝐶 ∈ 𝐴)
3		rabid 3435	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↔ (𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴))
4	3	simplbi2com 508	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐶 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}))
5	2, 4	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐶) → (𝑦 ∈ 𝐵 → 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}))
6	5	impancom 457	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐶 → 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}))
7	6	ancrd 561	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐶 → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)))
8	7	expimpd 459	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐶) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)))
9	8	reximdv2 3174	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶))
10	9	ralimia 3098	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶)
11	3	simplbi 502	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} → 𝑦 ∈ 𝐵)
12	6	pm4.71rd 572	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐶 ↔ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)))
13		df-mpt 5191	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶) = {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)}
14	13	breqi 5113	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ 𝑦{⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)}𝑥)
15		df-br 5108	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦{⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)}𝑥 ↔ ⟨𝑦, 𝑥⟩ ∈ {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)})
16		opabidw 5506	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑦, 𝑥⟩ ∈ {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)} ↔ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶))
17	14, 15, 16	3bitri 300	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶))
18	12, 17	bitr4di 292	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐶 ↔ 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
19	11, 18	sylan2 605	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}) → (𝑥 = 𝐶 ↔ 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
20	19	rexbidva 3186	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶 ↔ ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
21	20	ralbiia 3108	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
22		breq2 5111	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑥 → (𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
23	22	rexbidv 3188	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑥 → (∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
24		nfcv 2924	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑏{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}
25		nfrab1 3434	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}
26		nfcv 2924	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦𝑏
27		nfmpt1 5208	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)
28		nfcv 2924	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦𝑥
29	26, 27, 28	nfbr 5156	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥
30		nfv 1947	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑏 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥
31		breq1 5110	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑦 → (𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
32	24, 25, 29, 30, 31	cbvrexfw 3305	. . . . . . . . . . . . . . 15 ⊢ (∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
33	23, 32	bitrdi 290	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑥 → (∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
34	33	cbvralvw 3242	. . . . . . . . . . . . 13 ⊢ (∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
35	21, 34	bitr4i 281	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶 ↔ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎)
36	10, 35	sylib 221	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎)
37		nfv 1947	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)
38	25	nfcri 2916	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦 𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}
39		nfcsb1v 3874	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦⦋𝑏 / 𝑦⦌𝐶
40	39	nfeq2 2941	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦 𝑥 = ⦋𝑏 / 𝑦⦌𝐶
41	38, 40	nfan 1932	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦(𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶)
42		eleq1 2850	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑏 → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↔ 𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}))
43		csbeq1a 3864	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑏 → 𝐶 = ⦋𝑏 / 𝑦⦌𝐶)
44	43	eqeq2d 2773	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑏 → (𝑥 = 𝐶 ↔ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶))
45	42, 44	anbi12d 644	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑏 → ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶) ↔ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶)))
46	37, 41, 45	cbvopab1 5183	. . . . . . . . . . . . 13 ⊢ {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)} = {⟨𝑏, 𝑥⟩ ∣ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶)}
47		df-mpt 5191	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ ⦋𝑏 / 𝑦⦌𝐶) = {⟨𝑏, 𝑥⟩ ∣ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶)}
48	46, 13, 47	3eqtr4i 2795	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶) = (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ ⦋𝑏 / 𝑦⦌𝐶)
49		nfcv 2924	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦𝐵
50	39	nfel1 2940	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦⦋𝑏 / 𝑦⦌𝐶 ∈ 𝐴
51	43	eleq1d 2847	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑏 → (𝐶 ∈ 𝐴 ↔ ⦋𝑏 / 𝑦⦌𝐶 ∈ 𝐴))
52	26, 49, 50, 51	elrabf 3645	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↔ (𝑏 ∈ 𝐵 ∧ ⦋𝑏 / 𝑦⦌𝐶 ∈ 𝐴))
53	52	simprbi 503	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} → ⦋𝑏 / 𝑦⦌𝐶 ∈ 𝐴)
54	48, 53	fmpti 7109	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}⟶𝐴
55	36, 54	jctil 529	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}⟶𝐴 ∧ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎))
56		dffo4 7100	. . . . . . . . . 10 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴 ↔ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}⟶𝐴 ∧ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎))
57	55, 56	sylibr 237	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴)
58	57	adantl 487	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴)
59		relen 8961	. . . . . . . . . . . . 13 ⊢ Rel ≈
60	59	brrelex2i 5716	. . . . . . . . . . . 12 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ∈ V)
61		ssrab2 4031	. . . . . . . . . . . 12 ⊢ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ⊆ 𝐵
62		ssdomg 9010	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ V → ({𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ⊆ 𝐵 → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐵))
63	60, 61, 62	mpisyl 22	. . . . . . . . . . 11 ⊢ (𝐴 ≈ 𝐵 → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐵)
64		ensym 9013	. . . . . . . . . . 11 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)
65		domentr 9023	. . . . . . . . . . 11 ⊢ (({𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐵 ∧ 𝐵 ≈ 𝐴) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐴)
66	63, 64, 65	syl2anc 596	. . . . . . . . . 10 ⊢ (𝐴 ≈ 𝐵 → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐴)
67	66	ad2antlr 740	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐴)
68		enfi 9185	. . . . . . . . . . . 12 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Fin ↔ 𝐵 ∈ Fin))
69	68	biimpac 484	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐵 ∈ Fin)
70		rabfi 9245	. . . . . . . . . . 11 ⊢ (𝐵 ∈ Fin → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∈ Fin)
71	69, 70	syl 18	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∈ Fin)
72		fodomfi 9286	. . . . . . . . . 10 ⊢ (({𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∈ Fin ∧ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴) → 𝐴 ≼ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴})
73	71, 57, 72	syl2an 608	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → 𝐴 ≼ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴})
74		sbth 9099	. . . . . . . . 9 ⊢ (({𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐴 ∧ 𝐴 ≼ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≈ 𝐴)
75	67, 73, 74	syl2anc 596	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≈ 𝐴)
76		simpll 779	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → 𝐴 ∈ Fin)
77		fofinf1o 9303	. . . . . . . 8 ⊢ (((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴 ∧ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≈ 𝐴 ∧ 𝐴 ∈ Fin) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1-onto→𝐴)
78	58, 75, 76, 77	syl3anc 1398	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1-onto→𝐴)
79		f1of1 6820	. . . . . . 7 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1-onto→𝐴 → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴)
80	78, 79	syl 18	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴)
81		dff12 6774	. . . . . . . 8 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴 ↔ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}⟶𝐴 ∧ ∀𝑎∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎))
82	81	simprbi 503	. . . . . . 7 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴 → ∀𝑎∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎)
83	22	mobidv 2576	. . . . . . . . 9 ⊢ (𝑎 = 𝑥 → (∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
84	29, 30, 31	cbvmow 2630	. . . . . . . . 9 ⊢ (∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ ∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
85	83, 84	bitrdi 290	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → (∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
86	85	cbvalvw 2069	. . . . . . 7 ⊢ (∀𝑎∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∀𝑥∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
87	82, 86	sylib 221	. . . . . 6 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴 → ∀𝑥∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
88		mormo 3372	. . . . . . 7 ⊢ (∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 → ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
89	88	alimi 1844	. . . . . 6 ⊢ (∀𝑥∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 → ∀𝑥∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
90		alral 3093	. . . . . 6 ⊢ (∀𝑥∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 → ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
91	80, 87, 89, 90	4syl 20	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
92	18	rmobidva 3380	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 → (∃*𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
93	92	ralbiia 3108	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
94	91, 93	sylibr 237	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶)
95	94	ex 418	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
96	95	pm4.71d 571	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶)))
97		reu5 3369	. . . 4 ⊢ (∃!𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ (∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
98	97	ralbii 3110	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
99		r19.26 3124	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
100	98, 99	bitri 278	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
101	96, 100	bitr4di 292	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥 = 𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570   ∈ wcel 2145  ∃*wmo 2564  ∀wral 3078  ∃wrex 3088  ∃!wreu 3365  ∃*wrmo 3366  {crab 3414  Vcvv 3453  ⦋csb 3850   ⊆ wss 3902  ⟨cop 4593   class class class wbr 5107  {copab 5171   ↦ cmpt 5190  ⟶wf 6533  –1-1→wf1 6534  –onto→wfo 6535  –1-1-onto→wf1o 6536   ≈ cen 8953   ≼ cdom 8954  Fincfn 8956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-om 7867  df-1o 8459  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-fin 8960

This theorem is used by:  poimirlem25  38402  poimirlem26  38403