Theorem finminlem 31482

Description: A useful lemma about finite sets. If a property holds for a finite set, it holds for a minimal set. (Contributed by Jeff Hankins, 4-Dec-2009.)

Hypothesis

Ref	Expression
finminlem.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
finminlem	⊢ (∃𝑥 ∈ Fin 𝜑 → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦)))

Distinct variable groups:   𝜑,𝑦   𝜓,𝑥   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem finminlem

Dummy variables 𝑘 𝑚 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfe1 2014	. . . . 5 ⊢ Ⅎ𝑥∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)
2		nfcv 2751	. . . . 5 ⊢ Ⅎ𝑥ω
3	1, 2	nfrab 3100	. . . 4 ⊢ Ⅎ𝑥{𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)}
4		nfcv 2751	. . . 4 ⊢ Ⅎ𝑥∅
5	3, 4	nfne 2882	. . 3 ⊢ Ⅎ𝑥{𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅
6		isfi 7865	. . . 4 ⊢ (𝑥 ∈ Fin ↔ ∃𝑚 ∈ ω 𝑥 ≈ 𝑚)
7		19.8a 2039	. . . . . . . . . 10 ⊢ ((𝑥 ≈ 𝑚 ∧ 𝜑) → ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑))
8	7	anim2i 591	. . . . . . . . 9 ⊢ ((𝑚 ∈ ω ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝑚 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑)))
9	8	3impb 1252	. . . . . . . 8 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚 ∧ 𝜑) → (𝑚 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑)))
10		breq2 4587	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑚 → (𝑥 ≈ 𝑛 ↔ 𝑥 ≈ 𝑚))
11	10	anbi1d 737	. . . . . . . . . 10 ⊢ (𝑛 = 𝑚 → ((𝑥 ≈ 𝑛 ∧ 𝜑) ↔ (𝑥 ≈ 𝑚 ∧ 𝜑)))
12	11	exbidv 1837	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑) ↔ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑)))
13	12	elrab 3331	. . . . . . . 8 ⊢ (𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ↔ (𝑚 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑)))
14	9, 13	sylibr 223	. . . . . . 7 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚 ∧ 𝜑) → 𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)})
15		ne0i 3880	. . . . . . 7 ⊢ (𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅)
16	14, 15	syl 17	. . . . . 6 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚 ∧ 𝜑) → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅)
17	16	3exp 1256	. . . . 5 ⊢ (𝑚 ∈ ω → (𝑥 ≈ 𝑚 → (𝜑 → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅)))
18	17	rexlimiv 3009	. . . 4 ⊢ (∃𝑚 ∈ ω 𝑥 ≈ 𝑚 → (𝜑 → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅))
19	6, 18	sylbi 206	. . 3 ⊢ (𝑥 ∈ Fin → (𝜑 → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅))
20	5, 19	rexlimi 3006	. 2 ⊢ (∃𝑥 ∈ Fin 𝜑 → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅)
21		epweon 6875	. . 3 ⊢ E We On
22		ssrab2 3650	. . . 4 ⊢ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ⊆ ω
23		omsson 6961	. . . 4 ⊢ ω ⊆ On
24	22, 23	sstri 3577	. . 3 ⊢ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ⊆ On
25		wefrc 5032	. . 3 ⊢ (( E We On ∧ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ⊆ On ∧ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅) → ∃𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅)
26	21, 24, 25	mp3an12 1406	. 2 ⊢ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅ → ∃𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅)
27		nfv 1830	. . . . . . 7 ⊢ Ⅎ𝑥 𝑚 ∈ ω
28		nfcv 2751	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑚
29	3, 28	nfin 3782	. . . . . . . 8 ⊢ Ⅎ𝑥({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚)
30	29	nfeq1 2764	. . . . . . 7 ⊢ Ⅎ𝑥({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅
31	27, 30	nfan 1816	. . . . . 6 ⊢ Ⅎ𝑥(𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅)
32		simprr 792	. . . . . . . 8 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → 𝜑)
33		sspss 3668	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ 𝑥 ↔ (𝑦 ⊊ 𝑥 ∨ 𝑦 = 𝑥))
34		rspe 2986	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚) → ∃𝑚 ∈ ω 𝑥 ≈ 𝑚)
35		pssss 3664	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ⊊ 𝑥 → 𝑦 ⊆ 𝑥)
36		ssfi 8065	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ Fin ∧ 𝑦 ⊆ 𝑥) → 𝑦 ∈ Fin)
37	35, 36	sylan2 490	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ Fin ∧ 𝑦 ⊊ 𝑥) → 𝑦 ∈ Fin)
38	37	ex 449	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ Fin → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin))
39	6, 38	sylbir 224	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃𝑚 ∈ ω 𝑥 ≈ 𝑚 → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin))
40	34, 39	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚) → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin))
41	40	adantrr 749	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 ∈ ω ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin))
42	41	adantrr 749	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin))
43		isfi 7865	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ Fin ↔ ∃𝑘 ∈ ω 𝑦 ≈ 𝑘)
44		simprll 798	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝑘 ∈ ω)
45		simprlr 799	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝑦 ≈ 𝑘)
46		simplrr 797	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝜓)
47		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 𝑦 ∈ V
48		breq1 4586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑘 ↔ 𝑦 ≈ 𝑘))
49		finminlem.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
50	48, 49	anbi12d 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝑦 → ((𝑥 ≈ 𝑘 ∧ 𝜑) ↔ (𝑦 ≈ 𝑘 ∧ 𝜓)))
51	47, 50	spcev 3273	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑦 ≈ 𝑘 ∧ 𝜓) → ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑))
52	45, 46, 51	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑))
53	34, 6	sylibr 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚) → 𝑥 ∈ Fin)
54	53	adantrr 749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑚 ∈ ω ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → 𝑥 ∈ Fin)
55	54	adantrr 749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → 𝑥 ∈ Fin)
56	55	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → 𝑥 ∈ Fin)
57		php3 8031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑥 ∈ Fin ∧ 𝑦 ⊊ 𝑥) → 𝑦 ≺ 𝑥)
58	57	ex 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ Fin → (𝑦 ⊊ 𝑥 → 𝑦 ≺ 𝑥))
59	56, 58	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑦 ⊊ 𝑥 → 𝑦 ≺ 𝑥))
60		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑘 ∈ V
61		ssdomg 7887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 ∈ V → (𝑚 ⊆ 𝑘 → 𝑚 ≼ 𝑘))
62	60, 61	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 ⊆ 𝑘 → 𝑚 ≼ 𝑘)
63		endomtr 7900	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑥 ≈ 𝑚 ∧ 𝑚 ≼ 𝑘) → 𝑥 ≼ 𝑘)
64	63	ex 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑥 ≈ 𝑚 → (𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑘))
65	64	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓) → (𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑘))
66	65	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑘))
67		ensym 7891	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 ≈ 𝑘 → 𝑘 ≈ 𝑦)
68		domentr 7901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑥 ≼ 𝑘 ∧ 𝑘 ≈ 𝑦) → 𝑥 ≼ 𝑦)
69	67, 68	sylan2 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥 ≼ 𝑘 ∧ 𝑦 ≈ 𝑘) → 𝑥 ≼ 𝑦)
70	69	expcom 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 ≈ 𝑘 → (𝑥 ≼ 𝑘 → 𝑥 ≼ 𝑦))
71	70	ad2antll 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑥 ≼ 𝑘 → 𝑥 ≼ 𝑦))
72	66, 71	syld 46	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑦))
73	62, 72	syl5 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑚 ⊆ 𝑘 → 𝑥 ≼ 𝑦))
74		domnsym 7971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 ≼ 𝑦 → ¬ 𝑦 ≺ 𝑥)
75	74	con2i 133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 ≺ 𝑥 → ¬ 𝑥 ≼ 𝑦)
76	73, 75	nsyli 154	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑦 ≺ 𝑥 → ¬ 𝑚 ⊆ 𝑘))
77	59, 76	syld 46	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑦 ⊊ 𝑥 → ¬ 𝑚 ⊆ 𝑘))
78	77	impr 647	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → ¬ 𝑚 ⊆ 𝑘)
79		nnord 6965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑚 ∈ ω → Ord 𝑚)
80	79	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → Ord 𝑚)
81		nnord 6965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 ∈ ω → Ord 𝑘)
82	81	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) → Ord 𝑘)
83	82	ad2antrl 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → Ord 𝑘)
84		ordtri1 5673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((Ord 𝑚 ∧ Ord 𝑘) → (𝑚 ⊆ 𝑘 ↔ ¬ 𝑘 ∈ 𝑚))
85	84	con2bid 343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((Ord 𝑚 ∧ Ord 𝑘) → (𝑘 ∈ 𝑚 ↔ ¬ 𝑚 ⊆ 𝑘))
86	80, 83, 85	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → (𝑘 ∈ 𝑚 ↔ ¬ 𝑚 ⊆ 𝑘))
87	78, 86	mpbird 246	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝑘 ∈ 𝑚)
88	44, 52, 87	jca31 555	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → ((𝑘 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)) ∧ 𝑘 ∈ 𝑚))
89		elin 3758	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ↔ (𝑘 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∧ 𝑘 ∈ 𝑚))
90		breq2 4587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = 𝑘 → (𝑥 ≈ 𝑛 ↔ 𝑥 ≈ 𝑘))
91	90	anbi1d 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = 𝑘 → ((𝑥 ≈ 𝑛 ∧ 𝜑) ↔ (𝑥 ≈ 𝑘 ∧ 𝜑)))
92	91	exbidv 1837	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑘 → (∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑) ↔ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)))
93	92	elrab 3331	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ↔ (𝑘 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)))
94	93	anbi1i 727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∧ 𝑘 ∈ 𝑚) ↔ ((𝑘 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)) ∧ 𝑘 ∈ 𝑚))
95	89, 94	bitri 263	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 ∈ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ↔ ((𝑘 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)) ∧ 𝑘 ∈ 𝑚))
96	88, 95	sylibr 223	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝑘 ∈ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚))
97		ne0i 3880	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅)
98	96, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅)
99	98	exp44 639	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑘 ∈ ω → (𝑦 ≈ 𝑘 → (𝑦 ⊊ 𝑥 → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅))))
100	99	rexlimdv 3012	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (∃𝑘 ∈ ω 𝑦 ≈ 𝑘 → (𝑦 ⊊ 𝑥 → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅)))
101	43, 100	syl5bi 231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ∈ Fin → (𝑦 ⊊ 𝑥 → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅)))
102	101	com23 84	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊊ 𝑥 → (𝑦 ∈ Fin → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅)))
103	42, 102	mpdd 42	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊊ 𝑥 → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅))
104	103	necon2bd 2798	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ¬ 𝑦 ⊊ 𝑥))
105	104	ex 449	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ω → (((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓) → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ¬ 𝑦 ⊊ 𝑥)))
106	105	com23 84	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ω → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → (((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓) → ¬ 𝑦 ⊊ 𝑥)))
107	106	imp31 447	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → ¬ 𝑦 ⊊ 𝑥)
108	107	pm2.21d 117	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊊ 𝑥 → 𝑥 = 𝑦))
109		equcomi 1931	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
110	109	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 = 𝑥 → 𝑥 = 𝑦))
111	108, 110	jaod 394	. . . . . . . . . . . . 13 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → ((𝑦 ⊊ 𝑥 ∨ 𝑦 = 𝑥) → 𝑥 = 𝑦))
112	33, 111	syl5bi 231	. . . . . . . . . . . 12 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊆ 𝑥 → 𝑥 = 𝑦))
113	112	expr 641	. . . . . . . . . . 11 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝜓 → (𝑦 ⊆ 𝑥 → 𝑥 = 𝑦)))
114	113	com23 84	. . . . . . . . . 10 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝑦 ⊆ 𝑥 → (𝜓 → 𝑥 = 𝑦)))
115	114	impd 446	. . . . . . . . 9 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → ((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))
116	115	alrimiv 1842	. . . . . . . 8 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))
117	32, 116	jca 553	. . . . . . 7 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦)))
118	117	ex 449	. . . . . 6 ⊢ ((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) → ((𝑥 ≈ 𝑚 ∧ 𝜑) → (𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))))
119	31, 118	eximd 2072	. . . . 5 ⊢ ((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) → (∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑) → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))))
120	119	impancom 455	. . . 4 ⊢ ((𝑚 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑)) → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))))
121	13, 120	sylbi 206	. . 3 ⊢ (𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))))
122	121	rexlimiv 3009	. 2 ⊢ (∃𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦)))
123	20, 26, 122	3syl 18	1 ⊢ (∃𝑥 ∈ Fin 𝜑 → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∃wrex 2897  {crab 2900  Vcvv 3173   ∩ cin 3539   ⊆ wss 3540   ⊊ wpss 3541  ∅c0 3874   class class class wbr 4583   E cep 4947   We wwe 4996  Ord word 5639  Oncon0 5640  ωcom 6957   ≈ cen 7838   ≼ cdom 7839   ≺ csdm 7840  Fincfn 7841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-om 6958  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845

This theorem is referenced by: (None)