Theorem phpreu 37583

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 2816	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝐶 → (𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴))
2	1	biimpac 478	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐶) → 𝐶 ∈ 𝐴)
3		rabid 3418	. . . . . . . . . . . . . . . . . . 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 3139	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶))
10	9	ralimia 3063	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶)
11	3	simplbi 497	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} → 𝑦 ∈ 𝐵)
12	6	pm4.71rd 562	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐶 ↔ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)))
13		df-mpt 5177	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶) = {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)}
14	13	breqi 5101	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ 𝑦{⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)}𝑥)
15		df-br 5096	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦{⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)}𝑥 ↔ ⟨𝑦, 𝑥⟩ ∈ {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)})
16		opabidw 5471	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑦, 𝑥⟩ ∈ {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)} ↔ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶))
17	14, 15, 16	3bitri 297	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶))
18	12, 17	bitr4di 289	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐶 ↔ 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
19	11, 18	sylan2 593	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}) → (𝑥 = 𝐶 ↔ 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
20	19	rexbidva 3151	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶 ↔ ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
21	20	ralbiia 3073	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
22		breq2 5099	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑥 → (𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
23	22	rexbidv 3153	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑥 → (∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
24		nfcv 2891	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑏{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}
25		nfrab1 3417	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}
26		nfcv 2891	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦𝑏
27		nfmpt1 5194	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)
28		nfcv 2891	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦𝑥
29	26, 27, 28	nfbr 5142	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥
30		nfv 1914	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑏 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥
31		breq1 5098	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑦 → (𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
32	24, 25, 29, 30, 31	cbvrexfw 3271	. . . . . . . . . . . . . . 15 ⊢ (∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
33	23, 32	bitrdi 287	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑥 → (∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
34	33	cbvralvw 3207	. . . . . . . . . . . . 13 ⊢ (∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
35	21, 34	bitr4i 278	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑥 = 𝐶 ↔ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎)
36	10, 35	sylib 218	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎)
37		nfv 1914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)
38	25	nfcri 2883	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦 𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}
39		nfcsb1v 3877	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦⦋𝑏 / 𝑦⦌𝐶
40	39	nfeq2 2909	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦 𝑥 = ⦋𝑏 / 𝑦⦌𝐶
41	38, 40	nfan 1899	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦(𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶)
42		eleq1 2816	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑏 → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↔ 𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}))
43		csbeq1a 3867	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑏 → 𝐶 = ⦋𝑏 / 𝑦⦌𝐶)
44	43	eqeq2d 2740	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑏 → (𝑥 = 𝐶 ↔ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶))
45	42, 44	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑏 → ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶) ↔ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶)))
46	37, 41, 45	cbvopab1 5169	. . . . . . . . . . . . 13 ⊢ {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = 𝐶)} = {⟨𝑏, 𝑥⟩ ∣ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶)}
47		df-mpt 5177	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ ⦋𝑏 / 𝑦⦌𝐶) = {⟨𝑏, 𝑥⟩ ∣ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∧ 𝑥 = ⦋𝑏 / 𝑦⦌𝐶)}
48	46, 13, 47	3eqtr4i 2762	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶) = (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ ⦋𝑏 / 𝑦⦌𝐶)
49		nfcv 2891	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦𝐵
50	39	nfel1 2908	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦⦋𝑏 / 𝑦⦌𝐶 ∈ 𝐴
51	43	eleq1d 2813	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑏 → (𝐶 ∈ 𝐴 ↔ ⦋𝑏 / 𝑦⦌𝐶 ∈ 𝐴))
52	26, 49, 50, 51	elrabf 3646	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↔ (𝑏 ∈ 𝐵 ∧ ⦋𝑏 / 𝑦⦌𝐶 ∈ 𝐴))
53	52	simprbi 496	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} → ⦋𝑏 / 𝑦⦌𝐶 ∈ 𝐴)
54	48, 53	fmpti 7050	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}⟶𝐴
55	36, 54	jctil 519	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}⟶𝐴 ∧ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎))
56		dffo4 7041	. . . . . . . . . 10 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴 ↔ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}⟶𝐴 ∧ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎))
57	55, 56	sylibr 234	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴)
58	57	adantl 481	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴)
59		relen 8884	. . . . . . . . . . . . 13 ⊢ Rel ≈
60	59	brrelex2i 5680	. . . . . . . . . . . 12 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ∈ V)
61		ssrab2 4033	. . . . . . . . . . . 12 ⊢ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ⊆ 𝐵
62		ssdomg 8932	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ V → ({𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ⊆ 𝐵 → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐵))
63	60, 61, 62	mpisyl 21	. . . . . . . . . . 11 ⊢ (𝐴 ≈ 𝐵 → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐵)
64		ensym 8935	. . . . . . . . . . 11 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)
65		domentr 8945	. . . . . . . . . . 11 ⊢ (({𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐵 ∧ 𝐵 ≈ 𝐴) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐴)
66	63, 64, 65	syl2anc 584	. . . . . . . . . 10 ⊢ (𝐴 ≈ 𝐵 → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐴)
67	66	ad2antlr 727	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐴)
68		enfi 9111	. . . . . . . . . . . 12 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Fin ↔ 𝐵 ∈ Fin))
69	68	biimpac 478	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐵 ∈ Fin)
70		rabfi 9172	. . . . . . . . . . 11 ⊢ (𝐵 ∈ Fin → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∈ Fin)
71	69, 70	syl 17	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∈ Fin)
72		fodomfi 9219	. . . . . . . . . 10 ⊢ (({𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ∈ Fin ∧ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴) → 𝐴 ≼ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴})
73	71, 57, 72	syl2an 596	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → 𝐴 ≼ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴})
74		sbth 9021	. . . . . . . . 9 ⊢ (({𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≼ 𝐴 ∧ 𝐴 ≼ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≈ 𝐴)
75	67, 73, 74	syl2anc 584	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≈ 𝐴)
76		simpll 766	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → 𝐴 ∈ Fin)
77		fofinf1o 9241	. . . . . . . 8 ⊢ (((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–onto→𝐴 ∧ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ≈ 𝐴 ∧ 𝐴 ∈ Fin) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1-onto→𝐴)
78	58, 75, 76, 77	syl3anc 1373	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1-onto→𝐴)
79		f1of1 6767	. . . . . . 7 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1-onto→𝐴 → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴)
80	78, 79	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴)
81		dff12 6723	. . . . . . . 8 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴 ↔ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}⟶𝐴 ∧ ∀𝑎∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎))
82	81	simprbi 496	. . . . . . 7 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴 → ∀𝑎∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎)
83	22	mobidv 2542	. . . . . . . . 9 ⊢ (𝑎 = 𝑥 → (∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
84	29, 30, 31	cbvmow 2596	. . . . . . . . 9 ⊢ (∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 ↔ ∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
85	83, 84	bitrdi 287	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → (∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
86	85	cbvalvw 2036	. . . . . . 7 ⊢ (∀𝑎∃*𝑏 𝑏(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑎 ↔ ∀𝑥∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
87	82, 86	sylib 218	. . . . . 6 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶):{𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴}–1-1→𝐴 → ∀𝑥∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
88		mormo 3350	. . . . . . 7 ⊢ (∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 → ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
89	88	alimi 1811	. . . . . 6 ⊢ (∀𝑥∃*𝑦 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 → ∀𝑥∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
90		alral 3058	. . . . . 6 ⊢ (∀𝑥∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥 → ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
91	80, 87, 89, 90	4syl 19	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
92	18	rmobidva 3360	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 → (∃*𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥))
93	92	ralbiia 3073	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑦(𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴} ↦ 𝐶)𝑥)
94	91, 93	sylibr 234	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶) → ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶)
95	94	ex 412	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
96	95	pm4.71d 561	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶)))
97		reu5 3347	. . . 4 ⊢ (∃!𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ (∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
98	97	ralbii 3075	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
99		r19.26 3089	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
100	98, 99	bitri 275	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝑥 = 𝐶))
101	96, 100	bitr4di 289	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540   ∈ wcel 2109  ∃*wmo 2531  ∀wral 3044  ∃wrex 3053  ∃!wreu 3343  ∃*wrmo 3344  {crab 3396  Vcvv 3438  ⦋csb 3853   ⊆ wss 3905  ⟨cop 4585   class class class wbr 5095  {copab 5157   ↦ cmpt 5176  ⟶wf 6482  –1-1→wf1 6483  –onto→wfo 6484  –1-1-onto→wf1o 6485   ≈ cen 8876   ≼ cdom 8877  Fincfn 8879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3345  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-om 7807  df-1o 8395  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883

This theorem is referenced by:  poimirlem25  37624  poimirlem26  37625