Theorem finminlem 36553

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 2161	. . . . 5 ⊢ Ⅎ𝑥∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)
2		nfcv 2902	. . . . 5 ⊢ Ⅎ𝑥ω
3	1, 2	nfrabw 3429	. . . 4 ⊢ Ⅎ𝑥{𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)}
4		nfcv 2902	. . . 4 ⊢ Ⅎ𝑥∅
5	3, 4	nfne 3036	. . 3 ⊢ Ⅎ𝑥{𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅
6		isfi 8919	. . . 4 ⊢ (𝑥 ∈ Fin ↔ ∃𝑚 ∈ ω 𝑥 ≈ 𝑚)
7		19.8a 2193	. . . . . . . . . 10 ⊢ ((𝑥 ≈ 𝑚 ∧ 𝜑) → ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑))
8	7	anim2i 623	. . . . . . . . 9 ⊢ ((𝑚 ∈ ω ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝑚 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑)))
9	8	3impb 1120	. . . . . . . 8 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚 ∧ 𝜑) → (𝑚 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑)))
10		breq2 5083	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑚 → (𝑥 ≈ 𝑛 ↔ 𝑥 ≈ 𝑚))
11	10	anbi1d 637	. . . . . . . . . 10 ⊢ (𝑛 = 𝑚 → ((𝑥 ≈ 𝑛 ∧ 𝜑) ↔ (𝑥 ≈ 𝑚 ∧ 𝜑)))
12	11	exbidv 1928	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑) ↔ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑)))
13	12	elrab 3636	. . . . . . . 8 ⊢ (𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ↔ (𝑚 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑)))
14	9, 13	sylibr 235	. . . . . . 7 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚 ∧ 𝜑) → 𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)})
15	14	ne0d 4277	. . . . . 6 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚 ∧ 𝜑) → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅)
16	15	3exp 1125	. . . . 5 ⊢ (𝑚 ∈ ω → (𝑥 ≈ 𝑚 → (𝜑 → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅)))
17	16	rexlimiv 3134	. . . 4 ⊢ (∃𝑚 ∈ ω 𝑥 ≈ 𝑚 → (𝜑 → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅))
18	6, 17	sylbi 218	. . 3 ⊢ (𝑥 ∈ Fin → (𝜑 → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅))
19	5, 18	rexlimi 3240	. 2 ⊢ (∃𝑥 ∈ Fin 𝜑 → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅)
20		epweon 7725	. . 3 ⊢ E We On
21		ssrab2 4018	. . . 4 ⊢ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ⊆ ω
22		omsson 7817	. . . 4 ⊢ ω ⊆ On
23	21, 22	sstri 3931	. . 3 ⊢ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ⊆ On
24		wefrc 5619	. . 3 ⊢ (( E We On ∧ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ⊆ On ∧ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅) → ∃𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅)
25	20, 23, 24	mp3an12 1459	. 2 ⊢ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅ → ∃𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅)
26		nfv 1921	. . . . . . 7 ⊢ Ⅎ𝑥 𝑚 ∈ ω
27		nfcv 2902	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑚
28	3, 27	nfin 4160	. . . . . . . 8 ⊢ Ⅎ𝑥({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚)
29	28	nfeq1 2917	. . . . . . 7 ⊢ Ⅎ𝑥({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅
30	26, 29	nfan 1906	. . . . . 6 ⊢ Ⅎ𝑥(𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅)
31		simprr 778	. . . . . . . 8 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → 𝜑)
32		sspss 4040	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ 𝑥 ↔ (𝑦 ⊊ 𝑥 ∨ 𝑦 = 𝑥))
33		rspe 3230	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚) → ∃𝑚 ∈ ω 𝑥 ≈ 𝑚)
34		pssss 4036	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ⊊ 𝑥 → 𝑦 ⊆ 𝑥)
35		ssfi 9104	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ Fin ∧ 𝑦 ⊆ 𝑥) → 𝑦 ∈ Fin)
36	34, 35	sylan2 599	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ Fin ∧ 𝑦 ⊊ 𝑥) → 𝑦 ∈ Fin)
37	36	ex 413	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ Fin → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin))
38	6, 37	sylbir 236	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃𝑚 ∈ ω 𝑥 ≈ 𝑚 → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin))
39	33, 38	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚) → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin))
40	39	adantrr 723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 ∈ ω ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin))
41	40	adantrr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin))
42		isfi 8919	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ Fin ↔ ∃𝑘 ∈ ω 𝑦 ≈ 𝑘)
43		simprll 784	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝑘 ∈ ω)
44		simprlr 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝑦 ≈ 𝑘)
45		simplrr 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝜓)
46		vex 3436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 𝑦 ∈ V
47		breq1 5082	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑘 ↔ 𝑦 ≈ 𝑘))
48		finminlem.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
49	47, 48	anbi12d 638	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝑦 → ((𝑥 ≈ 𝑘 ∧ 𝜑) ↔ (𝑦 ≈ 𝑘 ∧ 𝜓)))
50	46, 49	spcev 3551	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑦 ≈ 𝑘 ∧ 𝜓) → ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑))
51	44, 45, 50	syl2anc 590	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑))
52	33, 6	sylibr 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚) → 𝑥 ∈ Fin)
53	52	adantrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑚 ∈ ω ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → 𝑥 ∈ Fin)
54	53	adantrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → 𝑥 ∈ Fin)
55	54	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → 𝑥 ∈ Fin)
56		php3 9140	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑥 ∈ Fin ∧ 𝑦 ⊊ 𝑥) → 𝑦 ≺ 𝑥)
57	56	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ Fin → (𝑦 ⊊ 𝑥 → 𝑦 ≺ 𝑥))
58	55, 57	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑦 ⊊ 𝑥 → 𝑦 ≺ 𝑥))
59		vex 3436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑘 ∈ V
60		ssdomg 8944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 ∈ V → (𝑚 ⊆ 𝑘 → 𝑚 ≼ 𝑘))
61	59, 60	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 ⊆ 𝑘 → 𝑚 ≼ 𝑘)
62		endomtr 8956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑥 ≈ 𝑚 ∧ 𝑚 ≼ 𝑘) → 𝑥 ≼ 𝑘)
63	62	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑥 ≈ 𝑚 → (𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑘))
64	63	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓) → (𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑘))
65	64	ad2antlr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑘))
66		ensym 8947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 ≈ 𝑘 → 𝑘 ≈ 𝑦)
67		domentr 8957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑥 ≼ 𝑘 ∧ 𝑘 ≈ 𝑦) → 𝑥 ≼ 𝑦)
68	66, 67	sylan2 599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥 ≼ 𝑘 ∧ 𝑦 ≈ 𝑘) → 𝑥 ≼ 𝑦)
69	68	expcom 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 ≈ 𝑘 → (𝑥 ≼ 𝑘 → 𝑥 ≼ 𝑦))
70	69	ad2antll 735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑥 ≼ 𝑘 → 𝑥 ≼ 𝑦))
71	65, 70	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑦))
72	61, 71	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑚 ⊆ 𝑘 → 𝑥 ≼ 𝑦))
73		domnsym 9038	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑚 ∈ ω → Ord 𝑚)
79	78	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → Ord 𝑚)
80		nnord 7821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 ∈ ω → Ord 𝑘)
81	80	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) → Ord 𝑘)
82	81	ad2antrl 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → Ord 𝑘)
83		ordtri1 6350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((Ord 𝑚 ∧ Ord 𝑘) → (𝑚 ⊆ 𝑘 ↔ ¬ 𝑘 ∈ 𝑚))
84	83	con2bid 355	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((Ord 𝑚 ∧ Ord 𝑘) → (𝑘 ∈ 𝑚 ↔ ¬ 𝑚 ⊆ 𝑘))
85	79, 82, 84	syl2anc 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → (𝑘 ∈ 𝑚 ↔ ¬ 𝑚 ⊆ 𝑘))
86	77, 85	mpbird 258	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝑘 ∈ 𝑚)
87	43, 51, 86	jca31 519	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → ((𝑘 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)) ∧ 𝑘 ∈ 𝑚))
88		elin 3906	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ↔ (𝑘 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∧ 𝑘 ∈ 𝑚))
89		breq2 5083	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = 𝑘 → (𝑥 ≈ 𝑛 ↔ 𝑥 ≈ 𝑘))
90	89	anbi1d 637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = 𝑘 → ((𝑥 ≈ 𝑛 ∧ 𝜑) ↔ (𝑥 ≈ 𝑘 ∧ 𝜑)))
91	90	exbidv 1928	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑘 → (∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑) ↔ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)))
92	91	elrab 3636	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ↔ (𝑘 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)))
93	92	anbi1i 630	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∧ 𝑘 ∈ 𝑚) ↔ ((𝑘 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)) ∧ 𝑘 ∈ 𝑚))
94	88, 93	bitri 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 ∈ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ↔ ((𝑘 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)) ∧ 𝑘 ∈ 𝑚))
95	87, 94	sylibr 235	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝑘 ∈ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚))
96	95	ne0d 4277	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅)
97	96	exp44 438	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑘 ∈ ω → (𝑦 ≈ 𝑘 → (𝑦 ⊊ 𝑥 → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅))))
98	97	rexlimdv 3139	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (∃𝑘 ∈ ω 𝑦 ≈ 𝑘 → (𝑦 ⊊ 𝑥 → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅)))
99	42, 98	biimtrid 243	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ∈ Fin → (𝑦 ⊊ 𝑥 → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅)))
100	99	com23 86	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊊ 𝑥 → (𝑦 ∈ Fin → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅)))
101	41, 100	mpdd 43	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊊ 𝑥 → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅))
102	101	necon2bd 2951	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ¬ 𝑦 ⊊ 𝑥))
103	102	ex 413	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ω → (((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓) → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ¬ 𝑦 ⊊ 𝑥)))
104	103	com23 86	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ω → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → (((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓) → ¬ 𝑦 ⊊ 𝑥)))
105	104	imp31 418	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → ¬ 𝑦 ⊊ 𝑥)
106	105	pm2.21d 121	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊊ 𝑥 → 𝑥 = 𝑦))
107		equcomi 2024	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
108	107	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 = 𝑥 → 𝑥 = 𝑦))
109	106, 108	jaod 865	. . . . . . . . . . . . 13 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → ((𝑦 ⊊ 𝑥 ∨ 𝑦 = 𝑥) → 𝑥 = 𝑦))
110	32, 109	biimtrid 243	. . . . . . . . . . . 12 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊆ 𝑥 → 𝑥 = 𝑦))
111	110	expr 457	. . . . . . . . . . 11 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝜓 → (𝑦 ⊆ 𝑥 → 𝑥 = 𝑦)))
112	111	com23 86	. . . . . . . . . 10 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝑦 ⊆ 𝑥 → (𝜓 → 𝑥 = 𝑦)))
113	112	impd 411	. . . . . . . . 9 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → ((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))
114	113	alrimiv 1934	. . . . . . . 8 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))
115	31, 114	jca 516	. . . . . . 7 ⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦)))
116	115	ex 413	. . . . . 6 ⊢ ((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) → ((𝑥 ≈ 𝑚 ∧ 𝜑) → (𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))))
117	30, 116	eximd 2228	. . . . 5 ⊢ ((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) → (∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑) → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))))
118	117	impancom 452	. . . 4 ⊢ ((𝑚 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑)) → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))))
119	13, 118	sylbi 218	. . 3 ⊢ (𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))))
120	119	rexlimiv 3134	. 2 ⊢ (∃𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦)))
121	19, 25, 120	3syl 18	1 ⊢ (∃𝑥 ∈ Fin 𝜑 → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 853   ∧ w3a 1092  ∀wal 1545   = wceq 1547  ∃wex 1786   ∈ wcel 2119   ≠ wne 2935  ∃wrex 3064  {crab 3392  Vcvv 3432   ∩ cin 3889   ⊆ wss 3890   ⊊ wpss 3891  ∅c0 4268   class class class wbr 5079   E cep 5524   We wwe 5577  Ord word 6316  Oncon0 6317  ωcom 7813   ≈ cen 8887   ≼ cdom 8888   ≺ csdm 8889  Fincfn 8890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-om 7814  df-1o 8402  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894

This theorem is referenced by: (None)