Theorem finminlem 34434

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 2149	. . . . 5 ⊢ Ⅎ𝑥∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)
2		nfcv 2906	. . . . 5 ⊢ Ⅎ𝑥ω
3	1, 2	nfrabw 3311	. . . 4 ⊢ Ⅎ𝑥{𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)}
4		nfcv 2906	. . . 4 ⊢ Ⅎ𝑥∅
5	3, 4	nfne 3044	. . 3 ⊢ Ⅎ𝑥{𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅
6		isfi 8719	. . . 4 ⊢ (𝑥 ∈ Fin ↔ ∃𝑚 ∈ ω 𝑥 ≈ 𝑚)
7		19.8a 2176	. . . . . . . . . 10 ⊢ ((𝑥 ≈ 𝑚 ∧ 𝜑) → ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑))
8	7	anim2i 616	. . . . . . . . 9 ⊢ ((𝑚 ∈ ω ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝑚 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑)))
9	8	3impb 1113	. . . . . . . 8 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚 ∧ 𝜑) → (𝑚 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑)))
10		breq2 5074	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑚 → (𝑥 ≈ 𝑛 ↔ 𝑥 ≈ 𝑚))
11	10	anbi1d 629	. . . . . . . . . 10 ⊢ (𝑛 = 𝑚 → ((𝑥 ≈ 𝑛 ∧ 𝜑) ↔ (𝑥 ≈ 𝑚 ∧ 𝜑)))
12	11	exbidv 1925	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑) ↔ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑)))
13	12	elrab 3617	. . . . . . . 8 ⊢ (𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ↔ (𝑚 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑)))
14	9, 13	sylibr 233	. . . . . . 7 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚 ∧ 𝜑) → 𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)})
15	14	ne0d 4266	. . . . . 6 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚 ∧ 𝜑) → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅)
16	15	3exp 1117	. . . . 5 ⊢ (𝑚 ∈ ω → (𝑥 ≈ 𝑚 → (𝜑 → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅)))
17	16	rexlimiv 3208	. . . 4 ⊢ (∃𝑚 ∈ ω 𝑥 ≈ 𝑚 → (𝜑 → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅))
18	6, 17	sylbi 216	. . 3 ⊢ (𝑥 ∈ Fin → (𝜑 → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅))
19	5, 18	rexlimi 3243	. 2 ⊢ (∃𝑥 ∈ Fin 𝜑 → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅)
20		epweon 7603	. . 3 ⊢ E We On
21		ssrab2 4009	. . . 4 ⊢ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ⊆ ω
22		omsson 7691	. . . 4 ⊢ ω ⊆ On
23	21, 22	sstri 3926	. . 3 ⊢ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ⊆ On
24		wefrc 5574	. . 3 ⊢ (( E We On ∧ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ⊆ On ∧ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅) → ∃𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅)
25	20, 23, 24	mp3an12 1449	. 2 ⊢ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅ → ∃𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅)
26		nfv 1918	. . . . . . 7 ⊢ Ⅎ𝑥 𝑚 ∈ ω
27		nfcv 2906	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑚
28	3, 27	nfin 4147	. . . . . . . 8 ⊢ Ⅎ𝑥({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚)
29	28	nfeq1 2921	. . . . . . 7 ⊢ Ⅎ𝑥({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅
30	26, 29	nfan 1903	. . . . . 6 ⊢ Ⅎ𝑥(𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅)
31		simprr 769	. . . . . . . 8 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → 𝜑)
32		sspss 4030	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ 𝑥 ↔ (𝑦 ⊊ 𝑥 ∨ 𝑦 = 𝑥))
33		rspe 3232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚) → ∃𝑚 ∈ ω 𝑥 ≈ 𝑚)
34		pssss 4026	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ⊊ 𝑥 → 𝑦 ⊆ 𝑥)
35		ssfi 8918	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ Fin ∧ 𝑦 ⊆ 𝑥) → 𝑦 ∈ Fin)
36	34, 35	sylan2 592	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ Fin ∧ 𝑦 ⊊ 𝑥) → 𝑦 ∈ Fin)
37	36	ex 412	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ Fin → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin))
38	6, 37	sylbir 234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃𝑚 ∈ ω 𝑥 ≈ 𝑚 → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin))
39	33, 38	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚) → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin))
40	39	adantrr 713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 ∈ ω ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin))
41	40	adantrr 713	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin))
42		isfi 8719	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ Fin ↔ ∃𝑘 ∈ ω 𝑦 ≈ 𝑘)
43		simprll 775	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝑘 ∈ ω)
44		simprlr 776	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝑦 ≈ 𝑘)
45		simplrr 774	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝜓)
46		vex 3426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 𝑦 ∈ V
47		breq1 5073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑘 ↔ 𝑦 ≈ 𝑘))
48		finminlem.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
49	47, 48	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝑦 → ((𝑥 ≈ 𝑘 ∧ 𝜑) ↔ (𝑦 ≈ 𝑘 ∧ 𝜓)))
50	46, 49	spcev 3535	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑦 ≈ 𝑘 ∧ 𝜓) → ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑))
51	44, 45, 50	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑))
52	33, 6	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚) → 𝑥 ∈ Fin)
53	52	adantrr 713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑚 ∈ ω ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → 𝑥 ∈ Fin)
54	53	adantrr 713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → 𝑥 ∈ Fin)
55	54	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → 𝑥 ∈ Fin)
56		php3 8899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑥 ∈ Fin ∧ 𝑦 ⊊ 𝑥) → 𝑦 ≺ 𝑥)
57	56	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ Fin → (𝑦 ⊊ 𝑥 → 𝑦 ≺ 𝑥))
58	55, 57	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑦 ⊊ 𝑥 → 𝑦 ≺ 𝑥))
59		vex 3426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑘 ∈ V
60		ssdomg 8741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 ∈ V → (𝑚 ⊆ 𝑘 → 𝑚 ≼ 𝑘))
61	59, 60	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 ⊆ 𝑘 → 𝑚 ≼ 𝑘)
62		endomtr 8753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑥 ≈ 𝑚 ∧ 𝑚 ≼ 𝑘) → 𝑥 ≼ 𝑘)
63	62	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑥 ≈ 𝑚 → (𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑘))
64	63	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓) → (𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑘))
65	64	ad2antlr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑘))
66		ensym 8744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 ≈ 𝑘 → 𝑘 ≈ 𝑦)
67		domentr 8754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑥 ≼ 𝑘 ∧ 𝑘 ≈ 𝑦) → 𝑥 ≼ 𝑦)
68	66, 67	sylan2 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥 ≼ 𝑘 ∧ 𝑦 ≈ 𝑘) → 𝑥 ≼ 𝑦)
69	68	expcom 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 ≈ 𝑘 → (𝑥 ≼ 𝑘 → 𝑥 ≼ 𝑦))
70	69	ad2antll 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑥 ≼ 𝑘 → 𝑥 ≼ 𝑦))
71	65, 70	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑦))
72	61, 71	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑚 ⊆ 𝑘 → 𝑥 ≼ 𝑦))
73		domnsym 8839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 ≼ 𝑦 → ¬ 𝑦 ≺ 𝑥)
74	73	con2i 139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 ≺ 𝑥 → ¬ 𝑥 ≼ 𝑦)
75	72, 74	nsyli 157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑦 ≺ 𝑥 → ¬ 𝑚 ⊆ 𝑘))
76	58, 75	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑦 ⊊ 𝑥 → ¬ 𝑚 ⊆ 𝑘))
77	76	impr 454	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → ¬ 𝑚 ⊆ 𝑘)
78		nnord 7695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑚 ∈ ω → Ord 𝑚)
79	78	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → Ord 𝑚)
80		nnord 7695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 ∈ ω → Ord 𝑘)
81	80	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) → Ord 𝑘)
82	81	ad2antrl 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → Ord 𝑘)
83		ordtri1 6284	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((Ord 𝑚 ∧ Ord 𝑘) → (𝑚 ⊆ 𝑘 ↔ ¬ 𝑘 ∈ 𝑚))
84	83	con2bid 354	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((Ord 𝑚 ∧ Ord 𝑘) → (𝑘 ∈ 𝑚 ↔ ¬ 𝑚 ⊆ 𝑘))
85	79, 82, 84	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → (𝑘 ∈ 𝑚 ↔ ¬ 𝑚 ⊆ 𝑘))
86	77, 85	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝑘 ∈ 𝑚)
87	43, 51, 86	jca31 514	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → ((𝑘 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)) ∧ 𝑘 ∈ 𝑚))
88		elin 3899	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ↔ (𝑘 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∧ 𝑘 ∈ 𝑚))
89		breq2 5074	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = 𝑘 → (𝑥 ≈ 𝑛 ↔ 𝑥 ≈ 𝑘))
90	89	anbi1d 629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = 𝑘 → ((𝑥 ≈ 𝑛 ∧ 𝜑) ↔ (𝑥 ≈ 𝑘 ∧ 𝜑)))
91	90	exbidv 1925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑘 → (∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑) ↔ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)))
92	91	elrab 3617	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ↔ (𝑘 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)))
93	92	anbi1i 623	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∧ 𝑘 ∈ 𝑚) ↔ ((𝑘 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)) ∧ 𝑘 ∈ 𝑚))
94	88, 93	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 ∈ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ↔ ((𝑘 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)) ∧ 𝑘 ∈ 𝑚))
95	87, 94	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝑘 ∈ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚))
96	95	ne0d 4266	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅)
97	96	exp44 437	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑘 ∈ ω → (𝑦 ≈ 𝑘 → (𝑦 ⊊ 𝑥 → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅))))
98	97	rexlimdv 3211	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (∃𝑘 ∈ ω 𝑦 ≈ 𝑘 → (𝑦 ⊊ 𝑥 → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅)))
99	42, 98	syl5bi 241	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ∈ Fin → (𝑦 ⊊ 𝑥 → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅)))
100	99	com23 86	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊊ 𝑥 → (𝑦 ∈ Fin → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅)))
101	41, 100	mpdd 43	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊊ 𝑥 → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅))
102	101	necon2bd 2958	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ¬ 𝑦 ⊊ 𝑥))
103	102	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ω → (((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓) → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ¬ 𝑦 ⊊ 𝑥)))
104	103	com23 86	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ω → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → (((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓) → ¬ 𝑦 ⊊ 𝑥)))
105	104	imp31 417	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → ¬ 𝑦 ⊊ 𝑥)
106	105	pm2.21d 121	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊊ 𝑥 → 𝑥 = 𝑦))
107		equcomi 2021	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
108	107	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 = 𝑥 → 𝑥 = 𝑦))
109	106, 108	jaod 855	. . . . . . . . . . . . 13 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → ((𝑦 ⊊ 𝑥 ∨ 𝑦 = 𝑥) → 𝑥 = 𝑦))
110	32, 109	syl5bi 241	. . . . . . . . . . . 12 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊆ 𝑥 → 𝑥 = 𝑦))
111	110	expr 456	. . . . . . . . . . 11 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝜓 → (𝑦 ⊆ 𝑥 → 𝑥 = 𝑦)))
112	111	com23 86	. . . . . . . . . 10 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝑦 ⊆ 𝑥 → (𝜓 → 𝑥 = 𝑦)))
113	112	impd 410	. . . . . . . . 9 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → ((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))
114	113	alrimiv 1931	. . . . . . . 8 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))
115	31, 114	jca 511	. . . . . . 7 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦)))
116	115	ex 412	. . . . . 6 ⊢ ((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) → ((𝑥 ≈ 𝑚 ∧ 𝜑) → (𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))))
117	30, 116	eximd 2212	. . . . 5 ⊢ ((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) → (∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑) → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))))
118	117	impancom 451	. . . 4 ⊢ ((𝑚 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑)) → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))))
119	13, 118	sylbi 216	. . 3 ⊢ (𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))))
120	119	rexlimiv 3208	. 2 ⊢ (∃𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦)))
121	19, 25, 120	3syl 18	1 ⊢ (∃𝑥 ∈ Fin 𝜑 → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 843   ∧ w3a 1085  ∀wal 1537   = wceq 1539  ∃wex 1783   ∈ wcel 2108   ≠ wne 2942  ∃wrex 3064  {crab 3067  Vcvv 3422   ∩ cin 3882   ⊆ wss 3883   ⊊ wpss 3884  ∅c0 4253   class class class wbr 5070   E cep 5485   We wwe 5534  Ord word 6250  Oncon0 6251  ωcom 7687   ≈ cen 8688   ≼ cdom 8689   ≺ csdm 8690  Fincfn 8691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-om 7688  df-1o 8267  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-fin 8695

This theorem is referenced by: (None)