Theorem phpreu 34350

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 2848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝐶 → (𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴))
2	1	biimpac 471	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐶) → 𝐶 ∈ 𝐴)
3		rabid 3312	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↔ (𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴))
4	3	simplbi2com 495	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐶 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}))
5	2, 4	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐶) → (𝑦 ∈ 𝐵 → 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}))
6	5	impancom 444	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐶 → 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}))
7	6	ancrd 544	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐶 → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)))
8	7	expimpd 446	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐶) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)))
9	8	reximdv2 3211	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶))
10	9	ralimia 3103	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶)
11	3	simplbi 490	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} → 𝑦 ∈ 𝐵)
12	6	pm4.71rd 555	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐶 ↔ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)))
13		df-mpt 5006	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶) = {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)}
14	13	breqi 4932	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ 𝑦{⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)}𝑥)
15		df-br 4927	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦{⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)}𝑥 ↔ ⟨𝑦, 𝑥⟩ ∈ {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)})
16		opabid 5265	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑦, 𝑥⟩ ∈ {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)} ↔ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶))
17	14, 15, 16	3bitri 289	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶))
18	12, 17	syl6bbr 281	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐶 ↔ 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
19	11, 18	sylan2 584	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}) → (𝑥 = 𝐶 ↔ 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
20	19	rexbidva 3236	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶 ↔ ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
21	20	ralbiia 3109	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
22		breq2 4930	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑥 → (𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
23	22	rexbidv 3237	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑥 → (∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
24		nfcv 2927	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑏{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}
25		nfrab1 3319	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}
26		nfcv 2927	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦𝑏
27		nfmpt1 5022	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)
28		nfcv 2927	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦𝑥
29	26, 27, 28	nfbr 4973	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥
30		nfv 1874	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑏 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥
31		breq1 4929	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑦 → (𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
32	24, 25, 29, 30, 31	cbvrexf 3373	. . . . . . . . . . . . . . 15 ⊢ (∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
33	23, 32	syl6bb 279	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑥 → (∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
34	33	cbvralv 3378	. . . . . . . . . . . . 13 ⊢ (∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
35	21, 34	bitr4i 270	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶 ↔ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎)
36	10, 35	sylib 210	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎)
37		nfv 1874	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)
38	25	nfcri 2921	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦 𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}
39		nfcsb1v 3799	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦⦋𝑏 / 𝑦⦌𝐶
40	39	nfeq2 2942	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦 𝑥 = ⦋𝑏 / 𝑦⦌𝐶
41	38, 40	nfan 1863	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦(𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶)
42		eleq1 2848	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑏 → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↔ 𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}))
43		csbeq1a 3790	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑏 → 𝐶 = ⦋𝑏 / 𝑦⦌𝐶)
44	43	eqeq2d 2783	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑏 → (𝑥 = 𝐶 ↔ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶))
45	42, 44	anbi12d 622	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑏 → ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶) ↔ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶)))
46	37, 41, 45	cbvopab1 4999	. . . . . . . . . . . . 13 ⊢ {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)} = {⟨𝑏, 𝑥⟩ ∣ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶)}
47		df-mpt 5006	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ ⦋𝑏 / 𝑦⦌𝐶) = {⟨𝑏, 𝑥⟩ ∣ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶)}
48	46, 13, 47	3eqtr4i 2807	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶) = (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ ⦋𝑏 / 𝑦⦌𝐶)
49		nfcv 2927	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦𝐵
50	39	nfel1 2941	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦⦋𝑏 / 𝑦⦌𝐶 ∈ 𝐴
51	43	eleq1d 2845	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑏 → (𝐶 ∈ 𝐴 ↔ ⦋𝑏 / 𝑦⦌𝐶 ∈ 𝐴))
52	26, 49, 50, 51	elrabf 3586	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↔ (𝑏 ∈ 𝐵 ∧ ⦋𝑏 / 𝑦⦌𝐶 ∈ 𝐴))
53	52	simprbi 489	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} → ⦋𝑏 / 𝑦⦌𝐶 ∈ 𝐴)
54	48, 53	fmpti 6698	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}⟶𝐴
55	36, 54	jctil 512	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}⟶𝐴 ∧ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎))
56		dffo4 6691	. . . . . . . . . 10 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴 ↔ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}⟶𝐴 ∧ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎))
57	55, 56	sylibr 226	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴)
58	57	adantl 474	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴)
59		relen 8310	. . . . . . . . . . . . 13 ⊢ Rel ≈
60	59	brrelex2i 5456	. . . . . . . . . . . 12 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ∈ V)
61		ssrab2 3941	. . . . . . . . . . . 12 ⊢ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ⊆ 𝐵
62		ssdomg 8351	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ V → ({𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ⊆ 𝐵 → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐵))
63	60, 61, 62	mpisyl 21	. . . . . . . . . . 11 ⊢ (𝐴 ≈ 𝐵 → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐵)
64		ensym 8354	. . . . . . . . . . 11 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)
65		domentr 8364	. . . . . . . . . . 11 ⊢ (({𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐵 ∧ 𝐵 ≈ 𝐴) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐴)
66	63, 64, 65	syl2anc 576	. . . . . . . . . 10 ⊢ (𝐴 ≈ 𝐵 → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐴)
67	66	ad2antlr 715	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐴)
68		enfi 8528	. . . . . . . . . . . 12 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Fin ↔ 𝐵 ∈ Fin))
69	68	biimpac 471	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐵 ∈ Fin)
70		rabfi 8537	. . . . . . . . . . 11 ⊢ (𝐵 ∈ Fin → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∈ Fin)
71	69, 70	syl 17	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∈ Fin)
72		fodomfi 8591	. . . . . . . . . 10 ⊢ (({𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∈ Fin ∧ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴) → 𝐴 ≼ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴})
73	71, 57, 72	syl2an 587	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → 𝐴 ≼ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴})
74		sbth 8432	. . . . . . . . 9 ⊢ (({𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐴 ∧ 𝐴 ≼ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≈ 𝐴)
75	67, 73, 74	syl2anc 576	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≈ 𝐴)
76		simpll 755	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → 𝐴 ∈ Fin)
77		fofinf1o 8593	. . . . . . . 8 ⊢ (((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴 ∧ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≈ 𝐴 ∧ 𝐴 ∈ Fin) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1-onto→𝐴)
78	58, 75, 76, 77	syl3anc 1352	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1-onto→𝐴)
79		f1of1 6441	. . . . . . 7 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1-onto→𝐴 → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴)
80	78, 79	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴)
81		dff12 6401	. . . . . . . 8 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴 ↔ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}⟶𝐴 ∧ ∀𝑎∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎))
82	81	simprbi 489	. . . . . . 7 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴 → ∀𝑎∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎)
83	22	mobidv 2562	. . . . . . . . 9 ⊢ (𝑎 = 𝑥 → (∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
84	29, 30, 31	cbvmo 2637	. . . . . . . . 9 ⊢ (∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ ∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
85	83, 84	syl6bb 279	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → (∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
86	85	cbvalvw 1994	. . . . . . 7 ⊢ (∀𝑎∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∀𝑥∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
87	82, 86	sylib 210	. . . . . 6 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴 → ∀𝑥∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
88		mormo 3364	. . . . . . 7 ⊢ (∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 → ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
89	88	alimi 1775	. . . . . 6 ⊢ (∀𝑥∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 → ∀𝑥∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
90		alral 3099	. . . . . 6 ⊢ (∀𝑥∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 → ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
91	80, 87, 89, 90	4syl 19	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
92	18	rmobidva 3328	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 → (∃*𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
93	92	ralbiia 3109	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
94	91, 93	sylibr 226	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶)
95	94	ex 405	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
96	95	pm4.71d 554	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶)))
97		reu5 3365	. . . 4 ⊢ (∃!𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ (∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
98	97	ralbii 3110	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
99		r19.26 3115	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
100	98, 99	bitri 267	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
101	96, 100	syl6bbr 281	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387  ∀wal 1506   = wceq 1508   ∈ wcel 2051  ∃*wmo 2546  ∀wral 3083  ∃wrex 3084  ∃!wreu 3085  ∃*wrmo 3086  {crab 3087  Vcvv 3410  ⦋csb 3781   ⊆ wss 3824  ⟨cop 4442   class class class wbr 4926  {copab 4988   ↦ cmpt 5005  ⟶wf 6182  –1-1→wf1 6183  –onto→wfo 6184  –1-1-onto→wf1o 6185   ≈ cen 8302   ≼ cdom 8303  Fincfn 8305

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-ral 3088  df-rex 3089  df-reu 3090  df-rmo 3091  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-pss 3840  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-tp 4441  df-op 4443  df-uni 4710  df-br 4927  df-opab 4989  df-mpt 5006  df-tr 5028  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-we 5365  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-om 7396  df-1o 7904  df-er 8088  df-en 8306  df-dom 8307  df-sdom 8308  df-fin 8309

This theorem is referenced by:  poimirlem25  34391  poimirlem26  34392