Theorem phpreu 38067

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 2849	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝐶 → (𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴))
2	1	biimpac 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐶) → 𝐶 ∈ 𝐴)
3		rabid 3434	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↔ (𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴))
4	3	simplbi2com 506	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐶 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}))
5	2, 4	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐶) → (𝑦 ∈ 𝐵 → 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}))
6	5	impancom 455	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐶 → 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}))
7	6	ancrd 559	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐶 → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)))
8	7	expimpd 457	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐶) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)))
9	8	reximdv2 3171	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶))
10	9	ralimia 3095	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶)
11	3	simplbi 500	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} → 𝑦 ∈ 𝐵)
12	6	pm4.71rd 570	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐶 ↔ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)))
13		df-mpt 5181	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶) = {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)}
14	13	breqi 5105	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ 𝑦{⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)}𝑥)
15		df-br 5100	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦{⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)}𝑥 ↔ ⟨𝑦, 𝑥⟩ ∈ {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)})
16		opabidw 5493	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑦, 𝑥⟩ ∈ {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)} ↔ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶))
17	14, 15, 16	3bitri 299	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶))
18	12, 17	bitr4di 291	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐶 ↔ 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
19	11, 18	sylan2 602	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}) → (𝑥 = 𝐶 ↔ 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
20	19	rexbidva 3183	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶 ↔ ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
21	20	ralbiia 3105	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
22		breq2 5103	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑥 → (𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
23	22	rexbidv 3185	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑥 → (∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
24		nfcv 2923	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑏{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}
25		nfrab1 3433	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}
26		nfcv 2923	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦𝑏
27		nfmpt1 5198	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)
28		nfcv 2923	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦𝑥
29	26, 27, 28	nfbr 5146	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥
30		nfv 1933	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑏 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥
31		breq1 5102	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑦 → (𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
32	24, 25, 29, 30, 31	cbvrexfw 3302	. . . . . . . . . . . . . . 15 ⊢ (∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
33	23, 32	bitrdi 289	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑥 → (∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
34	33	cbvralvw 3239	. . . . . . . . . . . . 13 ⊢ (∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
35	21, 34	bitr4i 280	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶 ↔ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎)
36	10, 35	sylib 220	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎)
37		nfv 1933	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)
38	25	nfcri 2915	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦 𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}
39		nfcsb1v 3876	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦⦋𝑏 / 𝑦⦌𝐶
40	39	nfeq2 2940	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦 𝑥 = ⦋𝑏 / 𝑦⦌𝐶
41	38, 40	nfan 1918	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦(𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶)
42		eleq1 2849	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑏 → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↔ 𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}))
43		csbeq1a 3866	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑏 → 𝐶 = ⦋𝑏 / 𝑦⦌𝐶)
44	43	eqeq2d 2772	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑏 → (𝑥 = 𝐶 ↔ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶))
45	42, 44	anbi12d 641	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑏 → ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶) ↔ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶)))
46	37, 41, 45	cbvopab1 5173	. . . . . . . . . . . . 13 ⊢ {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)} = {⟨𝑏, 𝑥⟩ ∣ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶)}
47		df-mpt 5181	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ ⦋𝑏 / 𝑦⦌𝐶) = {⟨𝑏, 𝑥⟩ ∣ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶)}
48	46, 13, 47	3eqtr4i 2794	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶) = (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ ⦋𝑏 / 𝑦⦌𝐶)
49		nfcv 2923	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦𝐵
50	39	nfel1 2939	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦⦋𝑏 / 𝑦⦌𝐶 ∈ 𝐴
51	43	eleq1d 2846	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑏 → (𝐶 ∈ 𝐴 ↔ ⦋𝑏 / 𝑦⦌𝐶 ∈ 𝐴))
52	26, 49, 50, 51	elrabf 3647	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↔ (𝑏 ∈ 𝐵 ∧ ⦋𝑏 / 𝑦⦌𝐶 ∈ 𝐴))
53	52	simprbi 501	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} → ⦋𝑏 / 𝑦⦌𝐶 ∈ 𝐴)
54	48, 53	fmpti 7089	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}⟶𝐴
55	36, 54	jctil 527	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}⟶𝐴 ∧ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎))
56		dffo4 7080	. . . . . . . . . 10 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴 ↔ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}⟶𝐴 ∧ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎))
57	55, 56	sylibr 236	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴)
58	57	adantl 485	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴)
59		relen 8928	. . . . . . . . . . . . 13 ⊢ Rel ≈
60	59	brrelex2i 5702	. . . . . . . . . . . 12 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ∈ V)
61		ssrab2 4033	. . . . . . . . . . . 12 ⊢ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ⊆ 𝐵
62		ssdomg 8977	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ V → ({𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ⊆ 𝐵 → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐵))
63	60, 61, 62	mpisyl 21	. . . . . . . . . . 11 ⊢ (𝐴 ≈ 𝐵 → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐵)
64		ensym 8980	. . . . . . . . . . 11 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)
65		domentr 8990	. . . . . . . . . . 11 ⊢ (({𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐵 ∧ 𝐵 ≈ 𝐴) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐴)
66	63, 64, 65	syl2anc 593	. . . . . . . . . 10 ⊢ (𝐴 ≈ 𝐵 → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐴)
67	66	ad2antlr 737	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐴)
68		enfi 9151	. . . . . . . . . . . 12 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Fin ↔ 𝐵 ∈ Fin))
69	68	biimpac 482	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐵 ∈ Fin)
70		rabfi 9211	. . . . . . . . . . 11 ⊢ (𝐵 ∈ Fin → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∈ Fin)
71	69, 70	syl 17	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∈ Fin)
72		fodomfi 9252	. . . . . . . . . 10 ⊢ (({𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∈ Fin ∧ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴) → 𝐴 ≼ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴})
73	71, 57, 72	syl2an 605	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → 𝐴 ≼ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴})
74		sbth 9065	. . . . . . . . 9 ⊢ (({𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐴 ∧ 𝐴 ≼ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≈ 𝐴)
75	67, 73, 74	syl2anc 593	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≈ 𝐴)
76		simpll 776	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → 𝐴 ∈ Fin)
77		fofinf1o 9272	. . . . . . . 8 ⊢ (((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴 ∧ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≈ 𝐴 ∧ 𝐴 ∈ Fin) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1-onto→𝐴)
78	58, 75, 76, 77	syl3anc 1389	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1-onto→𝐴)
79		f1of1 6801	. . . . . . 7 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1-onto→𝐴 → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴)
80	78, 79	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴)
81		dff12 6755	. . . . . . . 8 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴 ↔ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}⟶𝐴 ∧ ∀𝑎∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎))
82	81	simprbi 501	. . . . . . 7 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴 → ∀𝑎∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎)
83	22	mobidv 2575	. . . . . . . . 9 ⊢ (𝑎 = 𝑥 → (∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
84	29, 30, 31	cbvmow 2629	. . . . . . . . 9 ⊢ (∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ ∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
85	83, 84	bitrdi 289	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → (∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
86	85	cbvalvw 2055	. . . . . . 7 ⊢ (∀𝑎∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∀𝑥∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
87	82, 86	sylib 220	. . . . . 6 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴 → ∀𝑥∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
88		mormo 3371	. . . . . . 7 ⊢ (∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 → ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
89	88	alimi 1830	. . . . . 6 ⊢ (∀𝑥∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 → ∀𝑥∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
90		alral 3090	. . . . . 6 ⊢ (∀𝑥∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 → ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
91	80, 87, 89, 90	4syl 19	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
92	18	rmobidva 3379	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 → (∃*𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
93	92	ralbiia 3105	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
94	91, 93	sylibr 236	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶)
95	94	ex 416	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
96	95	pm4.71d 569	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶)))
97		reu5 3368	. . . 4 ⊢ (∃!𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ (∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
98	97	ralbii 3107	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
99		r19.26 3121	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
100	98, 99	bitri 277	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
101	96, 100	bitr4di 291	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399  ∀wal 1557   = wceq 1559   ∈ wcel 2141  ∃*wmo 2563  ∀wral 3075  ∃wrex 3085  ∃!wreu 3364  ∃*wrmo 3365  {crab 3413  Vcvv 3453  ⦋csb 3852   ⊆ wss 3904  ⟨cop 4587   class class class wbr 5099  {copab 5161   ↦ cmpt 5180  ⟶wf 6513  –1-1→wf1 6514  –onto→wfo 6515  –1-1-onto→wf1o 6516   ≈ cen 8920   ≼ cdom 8921  Fincfn 8923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pow 5321  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5540  df-eprel 5545  df-po 5553  df-so 5554  df-fr 5598  df-we 5600  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-ord 6345  df-on 6346  df-lim 6347  df-suc 6348  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-fv 6525  df-om 7843  df-1o 8432  df-er 8673  df-en 8924  df-dom 8925  df-sdom 8926  df-fin 8927

This theorem is referenced by:  poimirlem25  38108  poimirlem26  38109