Theorem finminlem 34790

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 2147	. . . . 5 ⊢ Ⅎ𝑥∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)
2		nfcv 2907	. . . . 5 ⊢ Ⅎ𝑥ω
3	1, 2	nfrabw 3440	. . . 4 ⊢ Ⅎ𝑥{𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)}
4		nfcv 2907	. . . 4 ⊢ Ⅎ𝑥∅
5	3, 4	nfne 3045	. . 3 ⊢ Ⅎ𝑥{𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅
6		isfi 8916	. . . 4 ⊢ (𝑥 ∈ Fin ↔ ∃𝑚 ∈ ω 𝑥 ≈ 𝑚)
7		19.8a 2174	. . . . . . . . . 10 ⊢ ((𝑥 ≈ 𝑚 ∧ 𝜑) → ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑))
8	7	anim2i 617	. . . . . . . . 9 ⊢ ((𝑚 ∈ ω ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝑚 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑)))
9	8	3impb 1115	. . . . . . . 8 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚 ∧ 𝜑) → (𝑚 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑)))
10		breq2 5109	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑚 → (𝑥 ≈ 𝑛 ↔ 𝑥 ≈ 𝑚))
11	10	anbi1d 630	. . . . . . . . . 10 ⊢ (𝑛 = 𝑚 → ((𝑥 ≈ 𝑛 ∧ 𝜑) ↔ (𝑥 ≈ 𝑚 ∧ 𝜑)))
12	11	exbidv 1924	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑) ↔ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑)))
13	12	elrab 3645	. . . . . . . 8 ⊢ (𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ↔ (𝑚 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑)))
14	9, 13	sylibr 233	. . . . . . 7 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚 ∧ 𝜑) → 𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)})
15	14	ne0d 4295	. . . . . 6 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚 ∧ 𝜑) → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅)
16	15	3exp 1119	. . . . 5 ⊢ (𝑚 ∈ ω → (𝑥 ≈ 𝑚 → (𝜑 → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅)))
17	16	rexlimiv 3145	. . . 4 ⊢ (∃𝑚 ∈ ω 𝑥 ≈ 𝑚 → (𝜑 → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅))
18	6, 17	sylbi 216	. . 3 ⊢ (𝑥 ∈ Fin → (𝜑 → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅))
19	5, 18	rexlimi 3242	. 2 ⊢ (∃𝑥 ∈ Fin 𝜑 → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅)
20		epweon 7709	. . 3 ⊢ E We On
21		ssrab2 4037	. . . 4 ⊢ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ⊆ ω
22		omsson 7806	. . . 4 ⊢ ω ⊆ On
23	21, 22	sstri 3953	. . 3 ⊢ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ⊆ On
24		wefrc 5627	. . 3 ⊢ (( E We On ∧ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ⊆ On ∧ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅) → ∃𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅)
25	20, 23, 24	mp3an12 1451	. 2 ⊢ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅ → ∃𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅)
26		nfv 1917	. . . . . . 7 ⊢ Ⅎ𝑥 𝑚 ∈ ω
27		nfcv 2907	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑚
28	3, 27	nfin 4176	. . . . . . . 8 ⊢ Ⅎ𝑥({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚)
29	28	nfeq1 2922	. . . . . . 7 ⊢ Ⅎ𝑥({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅
30	26, 29	nfan 1902	. . . . . 6 ⊢ Ⅎ𝑥(𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅)
31		simprr 771	. . . . . . . 8 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → 𝜑)
32		sspss 4059	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ 𝑥 ↔ (𝑦 ⊊ 𝑥 ∨ 𝑦 = 𝑥))
33		rspe 3232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚) → ∃𝑚 ∈ ω 𝑥 ≈ 𝑚)
34		pssss 4055	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ⊊ 𝑥 → 𝑦 ⊆ 𝑥)
35		ssfi 9117	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ Fin ∧ 𝑦 ⊆ 𝑥) → 𝑦 ∈ Fin)
36	34, 35	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ Fin ∧ 𝑦 ⊊ 𝑥) → 𝑦 ∈ Fin)
37	36	ex 413	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ Fin → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin))
38	6, 37	sylbir 234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃𝑚 ∈ ω 𝑥 ≈ 𝑚 → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin))
39	33, 38	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚) → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin))
40	39	adantrr 715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 ∈ ω ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin))
41	40	adantrr 715	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin))
42		isfi 8916	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ Fin ↔ ∃𝑘 ∈ ω 𝑦 ≈ 𝑘)
43		simprll 777	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝑘 ∈ ω)
44		simprlr 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝑦 ≈ 𝑘)
45		simplrr 776	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝜓)
46		vex 3449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 𝑦 ∈ V
47		breq1 5108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑘 ↔ 𝑦 ≈ 𝑘))
48		finminlem.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
49	47, 48	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝑦 → ((𝑥 ≈ 𝑘 ∧ 𝜑) ↔ (𝑦 ≈ 𝑘 ∧ 𝜓)))
50	46, 49	spcev 3565	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑦 ≈ 𝑘 ∧ 𝜓) → ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑))
51	44, 45, 50	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑))
52	33, 6	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚) → 𝑥 ∈ Fin)
53	52	adantrr 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑚 ∈ ω ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → 𝑥 ∈ Fin)
54	53	adantrr 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → 𝑥 ∈ Fin)
55	54	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → 𝑥 ∈ Fin)
56		php3 9156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑥 ∈ Fin ∧ 𝑦 ⊊ 𝑥) → 𝑦 ≺ 𝑥)
57	56	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ Fin → (𝑦 ⊊ 𝑥 → 𝑦 ≺ 𝑥))
58	55, 57	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑦 ⊊ 𝑥 → 𝑦 ≺ 𝑥))
59		vex 3449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑘 ∈ V
60		ssdomg 8940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 ∈ V → (𝑚 ⊆ 𝑘 → 𝑚 ≼ 𝑘))
61	59, 60	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 ⊆ 𝑘 → 𝑚 ≼ 𝑘)
62		endomtr 8952	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑥 ≈ 𝑚 ∧ 𝑚 ≼ 𝑘) → 𝑥 ≼ 𝑘)
63	62	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑥 ≈ 𝑚 → (𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑘))
64	63	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓) → (𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑘))
65	64	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑘))
66		ensym 8943	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 ≈ 𝑘 → 𝑘 ≈ 𝑦)
67		domentr 8953	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑥 ≼ 𝑘 ∧ 𝑘 ≈ 𝑦) → 𝑥 ≼ 𝑦)
68	66, 67	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥 ≼ 𝑘 ∧ 𝑦 ≈ 𝑘) → 𝑥 ≼ 𝑦)
69	68	expcom 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 ≈ 𝑘 → (𝑥 ≼ 𝑘 → 𝑥 ≼ 𝑦))
70	69	ad2antll 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑥 ≼ 𝑘 → 𝑥 ≼ 𝑦))
71	65, 70	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑦))
72	61, 71	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑚 ⊆ 𝑘 → 𝑥 ≼ 𝑦))
73		domnsym 9043	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 ≼ 𝑦 → ¬ 𝑦 ≺ 𝑥)
74	73	con2i 139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 ≺ 𝑥 → ¬ 𝑥 ≼ 𝑦)
75	72, 74	nsyli 157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑦 ≺ 𝑥 → ¬ 𝑚 ⊆ 𝑘))
76	58, 75	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑦 ⊊ 𝑥 → ¬ 𝑚 ⊆ 𝑘))
77	76	impr 455	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → ¬ 𝑚 ⊆ 𝑘)
78		nnord 7810	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑚 ∈ ω → Ord 𝑚)
79	78	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → Ord 𝑚)
80		nnord 7810	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 ∈ ω → Ord 𝑘)
81	80	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) → Ord 𝑘)
82	81	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → Ord 𝑘)
83		ordtri1 6350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((Ord 𝑚 ∧ Ord 𝑘) → (𝑚 ⊆ 𝑘 ↔ ¬ 𝑘 ∈ 𝑚))
84	83	con2bid 354	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((Ord 𝑚 ∧ Ord 𝑘) → (𝑘 ∈ 𝑚 ↔ ¬ 𝑚 ⊆ 𝑘))
85	79, 82, 84	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → (𝑘 ∈ 𝑚 ↔ ¬ 𝑚 ⊆ 𝑘))
86	77, 85	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝑘 ∈ 𝑚)
87	43, 51, 86	jca31 515	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → ((𝑘 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)) ∧ 𝑘 ∈ 𝑚))
88		elin 3926	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ↔ (𝑘 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∧ 𝑘 ∈ 𝑚))
89		breq2 5109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = 𝑘 → (𝑥 ≈ 𝑛 ↔ 𝑥 ≈ 𝑘))
90	89	anbi1d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = 𝑘 → ((𝑥 ≈ 𝑛 ∧ 𝜑) ↔ (𝑥 ≈ 𝑘 ∧ 𝜑)))
91	90	exbidv 1924	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑘 → (∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑) ↔ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)))
92	91	elrab 3645	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ↔ (𝑘 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)))
93	92	anbi1i 624	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∧ 𝑘 ∈ 𝑚) ↔ ((𝑘 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)) ∧ 𝑘 ∈ 𝑚))
94	88, 93	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 ∈ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ↔ ((𝑘 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)) ∧ 𝑘 ∈ 𝑚))
95	87, 94	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝑘 ∈ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚))
96	95	ne0d 4295	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅)
97	96	exp44 438	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑘 ∈ ω → (𝑦 ≈ 𝑘 → (𝑦 ⊊ 𝑥 → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅))))
98	97	rexlimdv 3150	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (∃𝑘 ∈ ω 𝑦 ≈ 𝑘 → (𝑦 ⊊ 𝑥 → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅)))
99	42, 98	biimtrid 241	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ∈ Fin → (𝑦 ⊊ 𝑥 → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅)))
100	99	com23 86	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊊ 𝑥 → (𝑦 ∈ Fin → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅)))
101	41, 100	mpdd 43	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊊ 𝑥 → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅))
102	101	necon2bd 2959	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ¬ 𝑦 ⊊ 𝑥))
103	102	ex 413	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ω → (((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓) → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ¬ 𝑦 ⊊ 𝑥)))
104	103	com23 86	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ω → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → (((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓) → ¬ 𝑦 ⊊ 𝑥)))
105	104	imp31 418	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → ¬ 𝑦 ⊊ 𝑥)
106	105	pm2.21d 121	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊊ 𝑥 → 𝑥 = 𝑦))
107		equcomi 2020	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
108	107	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 = 𝑥 → 𝑥 = 𝑦))
109	106, 108	jaod 857	. . . . . . . . . . . . 13 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → ((𝑦 ⊊ 𝑥 ∨ 𝑦 = 𝑥) → 𝑥 = 𝑦))
110	32, 109	biimtrid 241	. . . . . . . . . . . 12 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊆ 𝑥 → 𝑥 = 𝑦))
111	110	expr 457	. . . . . . . . . . 11 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝜓 → (𝑦 ⊆ 𝑥 → 𝑥 = 𝑦)))
112	111	com23 86	. . . . . . . . . 10 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝑦 ⊆ 𝑥 → (𝜓 → 𝑥 = 𝑦)))
113	112	impd 411	. . . . . . . . 9 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → ((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))
114	113	alrimiv 1930	. . . . . . . 8 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))
115	31, 114	jca 512	. . . . . . 7 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦)))
116	115	ex 413	. . . . . 6 ⊢ ((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) → ((𝑥 ≈ 𝑚 ∧ 𝜑) → (𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))))
117	30, 116	eximd 2209	. . . . 5 ⊢ ((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) → (∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑) → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))))
118	117	impancom 452	. . . 4 ⊢ ((𝑚 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑)) → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))))
119	13, 118	sylbi 216	. . 3 ⊢ (𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))))
120	119	rexlimiv 3145	. 2 ⊢ (∃𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦)))
121	19, 25, 120	3syl 18	1 ⊢ (∃𝑥 ∈ Fin 𝜑 → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∧ w3a 1087  ∀wal 1539   = wceq 1541  ∃wex 1781   ∈ wcel 2106   ≠ wne 2943  ∃wrex 3073  {crab 3407  Vcvv 3445   ∩ cin 3909   ⊆ wss 3910   ⊊ wpss 3911  ∅c0 4282   class class class wbr 5105   E cep 5536   We wwe 5587  Ord word 6316  Oncon0 6317  ωcom 7802   ≈ cen 8880   ≼ cdom 8881   ≺ csdm 8882  Fincfn 8883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-om 7803  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887

This theorem is referenced by: (None)