Theorem phpreu 37591

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 2827	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝐶 → (𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴))
2	1	biimpac 478	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐶) → 𝐶 ∈ 𝐴)
3		rabid 3455	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↔ (𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴))
4	3	simplbi2com 502	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐶 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}))
5	2, 4	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐶) → (𝑦 ∈ 𝐵 → 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}))
6	5	impancom 451	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐶 → 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}))
7	6	ancrd 551	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐶 → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)))
8	7	expimpd 453	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐶) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)))
9	8	reximdv2 3162	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶))
10	9	ralimia 3078	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶)
11	3	simplbi 497	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} → 𝑦 ∈ 𝐵)
12	6	pm4.71rd 562	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐶 ↔ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)))
13		df-mpt 5232	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶) = {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)}
14	13	breqi 5154	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ 𝑦{⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)}𝑥)
15		df-br 5149	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦{⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)}𝑥 ↔ ⟨𝑦, 𝑥⟩ ∈ {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)})
16		opabidw 5534	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑦, 𝑥⟩ ∈ {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)} ↔ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶))
17	14, 15, 16	3bitri 297	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶))
18	12, 17	bitr4di 289	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐶 ↔ 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
19	11, 18	sylan2 593	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}) → (𝑥 = 𝐶 ↔ 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
20	19	rexbidva 3175	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶 ↔ ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
21	20	ralbiia 3089	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
22		breq2 5152	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑥 → (𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
23	22	rexbidv 3177	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑥 → (∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
24		nfcv 2903	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑏{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}
25		nfrab1 3454	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}
26		nfcv 2903	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦𝑏
27		nfmpt1 5256	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)
28		nfcv 2903	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦𝑥
29	26, 27, 28	nfbr 5195	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥
30		nfv 1912	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑏 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥
31		breq1 5151	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑦 → (𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
32	24, 25, 29, 30, 31	cbvrexfw 3303	. . . . . . . . . . . . . . 15 ⊢ (∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
33	23, 32	bitrdi 287	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑥 → (∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
34	33	cbvralvw 3235	. . . . . . . . . . . . 13 ⊢ (∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
35	21, 34	bitr4i 278	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶 ↔ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎)
36	10, 35	sylib 218	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎)
37		nfv 1912	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)
38	25	nfcri 2895	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦 𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}
39		nfcsb1v 3933	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦⦋𝑏 / 𝑦⦌𝐶
40	39	nfeq2 2921	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦 𝑥 = ⦋𝑏 / 𝑦⦌𝐶
41	38, 40	nfan 1897	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦(𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶)
42		eleq1 2827	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑏 → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↔ 𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}))
43		csbeq1a 3922	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑏 → 𝐶 = ⦋𝑏 / 𝑦⦌𝐶)
44	43	eqeq2d 2746	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑏 → (𝑥 = 𝐶 ↔ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶))
45	42, 44	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑏 → ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶) ↔ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶)))
46	37, 41, 45	cbvopab1 5223	. . . . . . . . . . . . 13 ⊢ {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)} = {⟨𝑏, 𝑥⟩ ∣ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶)}
47		df-mpt 5232	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ ⦋𝑏 / 𝑦⦌𝐶) = {⟨𝑏, 𝑥⟩ ∣ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶)}
48	46, 13, 47	3eqtr4i 2773	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶) = (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ ⦋𝑏 / 𝑦⦌𝐶)
49		nfcv 2903	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦𝐵
50	39	nfel1 2920	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦⦋𝑏 / 𝑦⦌𝐶 ∈ 𝐴
51	43	eleq1d 2824	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑏 → (𝐶 ∈ 𝐴 ↔ ⦋𝑏 / 𝑦⦌𝐶 ∈ 𝐴))
52	26, 49, 50, 51	elrabf 3691	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↔ (𝑏 ∈ 𝐵 ∧ ⦋𝑏 / 𝑦⦌𝐶 ∈ 𝐴))
53	52	simprbi 496	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} → ⦋𝑏 / 𝑦⦌𝐶 ∈ 𝐴)
54	48, 53	fmpti 7132	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}⟶𝐴
55	36, 54	jctil 519	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}⟶𝐴 ∧ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎))
56		dffo4 7123	. . . . . . . . . 10 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴 ↔ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}⟶𝐴 ∧ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎))
57	55, 56	sylibr 234	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴)
58	57	adantl 481	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴)
59		relen 8989	. . . . . . . . . . . . 13 ⊢ Rel ≈
60	59	brrelex2i 5746	. . . . . . . . . . . 12 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ∈ V)
61		ssrab2 4090	. . . . . . . . . . . 12 ⊢ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ⊆ 𝐵
62		ssdomg 9039	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ V → ({𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ⊆ 𝐵 → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐵))
63	60, 61, 62	mpisyl 21	. . . . . . . . . . 11 ⊢ (𝐴 ≈ 𝐵 → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐵)
64		ensym 9042	. . . . . . . . . . 11 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)
65		domentr 9052	. . . . . . . . . . 11 ⊢ (({𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐵 ∧ 𝐵 ≈ 𝐴) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐴)
66	63, 64, 65	syl2anc 584	. . . . . . . . . 10 ⊢ (𝐴 ≈ 𝐵 → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐴)
67	66	ad2antlr 727	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐴)
68		enfi 9225	. . . . . . . . . . . 12 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Fin ↔ 𝐵 ∈ Fin))
69	68	biimpac 478	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐵 ∈ Fin)
70		rabfi 9301	. . . . . . . . . . 11 ⊢ (𝐵 ∈ Fin → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∈ Fin)
71	69, 70	syl 17	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∈ Fin)
72		fodomfi 9348	. . . . . . . . . 10 ⊢ (({𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∈ Fin ∧ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴) → 𝐴 ≼ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴})
73	71, 57, 72	syl2an 596	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → 𝐴 ≼ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴})
74		sbth 9132	. . . . . . . . 9 ⊢ (({𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐴 ∧ 𝐴 ≼ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≈ 𝐴)
75	67, 73, 74	syl2anc 584	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≈ 𝐴)
76		simpll 767	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → 𝐴 ∈ Fin)
77		fofinf1o 9370	. . . . . . . 8 ⊢ (((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴 ∧ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≈ 𝐴 ∧ 𝐴 ∈ Fin) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1-onto→𝐴)
78	58, 75, 76, 77	syl3anc 1370	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1-onto→𝐴)
79		f1of1 6848	. . . . . . 7 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1-onto→𝐴 → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴)
80	78, 79	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴)
81		dff12 6804	. . . . . . . 8 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴 ↔ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}⟶𝐴 ∧ ∀𝑎∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎))
82	81	simprbi 496	. . . . . . 7 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴 → ∀𝑎∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎)
83	22	mobidv 2547	. . . . . . . . 9 ⊢ (𝑎 = 𝑥 → (∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
84	29, 30, 31	cbvmow 2601	. . . . . . . . 9 ⊢ (∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ ∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
85	83, 84	bitrdi 287	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → (∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
86	85	cbvalvw 2033	. . . . . . 7 ⊢ (∀𝑎∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∀𝑥∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
87	82, 86	sylib 218	. . . . . 6 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴 → ∀𝑥∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
88		mormo 3383	. . . . . . 7 ⊢ (∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 → ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
89	88	alimi 1808	. . . . . 6 ⊢ (∀𝑥∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 → ∀𝑥∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
90		alral 3073	. . . . . 6 ⊢ (∀𝑥∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 → ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
91	80, 87, 89, 90	4syl 19	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
92	18	rmobidva 3393	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 → (∃*𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
93	92	ralbiia 3089	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
94	91, 93	sylibr 234	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶)
95	94	ex 412	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
96	95	pm4.71d 561	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶)))
97		reu5 3380	. . . 4 ⊢ (∃!𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ (∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
98	97	ralbii 3091	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
99		r19.26 3109	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
100	98, 99	bitri 275	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
101	96, 100	bitr4di 289	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1535   = wceq 1537   ∈ wcel 2106  ∃*wmo 2536  ∀wral 3059  ∃wrex 3068  ∃!wreu 3376  ∃*wrmo 3377  {crab 3433  Vcvv 3478  ⦋csb 3908   ⊆ wss 3963  ⟨cop 4637   class class class wbr 5148  {copab 5210   ↦ cmpt 5231  ⟶wf 6559  –1-1→wf1 6560  –onto→wfo 6561  –1-1-onto→wf1o 6562   ≈ cen 8981   ≼ cdom 8982  Fincfn 8984

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-om 7888  df-1o 8505  df-er 8744  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988

This theorem is referenced by:  poimirlem25  37632  poimirlem26  37633