Metamath Proof Explorer

Theorem finminlem

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)

Ref Expression
Hypothesis finminlem.1 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion finminlem ( ∃ 𝑥 ∈ Fin 𝜑 → ∃ 𝑥 ( 𝜑 ∧ ∀ 𝑦 ( ( 𝑦 ⊆ 𝑥 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 finminlem.1 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2 nfe1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 )
3 nfcv ⊢ Ⅎ 𝑥 ω
4 2 3 nfrabw ⊢ Ⅎ 𝑥 { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) }
5 nfcv ⊢ Ⅎ 𝑥 ∅
6 4 5 nfne ⊢ Ⅎ 𝑥 { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ≠ ∅
7 isfi ⊢ ( 𝑥 ∈ Fin ↔ ∃ 𝑚 ∈ ω 𝑥 ≈ 𝑚 )
8 19.8a ⊢ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) → ∃ 𝑥 ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) )
9 8 anim2i ⊢ ( ( 𝑚 ∈ ω ∧ ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ) → ( 𝑚 ∈ ω ∧ ∃ 𝑥 ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ) )
10 9 3impb ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚 ∧ 𝜑 ) → ( 𝑚 ∈ ω ∧ ∃ 𝑥 ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ) )
11 breq2 ⊢ ( 𝑛 = 𝑚 → ( 𝑥 ≈ 𝑛 ↔ 𝑥 ≈ 𝑚 ) )
12 11 anbi1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) ↔ ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ) )
13 12 exbidv ⊢ ( 𝑛 = 𝑚 → ( ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ) )
14 13 elrab ⊢ ( 𝑚 ∈ { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ↔ ( 𝑚 ∈ ω ∧ ∃ 𝑥 ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ) )
15 10 14 sylibr ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚 ∧ 𝜑 ) → 𝑚 ∈ { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } )
16 15 ne0d ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚 ∧ 𝜑 ) → { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ≠ ∅ )
17 16 3exp ⊢ ( 𝑚 ∈ ω → ( 𝑥 ≈ 𝑚 → ( 𝜑 → { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ≠ ∅ ) ) )
18 17 rexlimiv ⊢ ( ∃ 𝑚 ∈ ω 𝑥 ≈ 𝑚 → ( 𝜑 → { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ≠ ∅ ) )
19 7 18 sylbi ⊢ ( 𝑥 ∈ Fin → ( 𝜑 → { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ≠ ∅ ) )
20 6 19 rexlimi ⊢ ( ∃ 𝑥 ∈ Fin 𝜑 → { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ≠ ∅ )
21 epweon ⊢ E We On
22 ssrab2 ⊢ { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ⊆ ω
23 omsson ⊢ ω ⊆ On
24 22 23 sstri ⊢ { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ⊆ On
25 wefrc ⊢ ( ( E We On ∧ { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ⊆ On ∧ { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ≠ ∅ ) → ∃ 𝑚 ∈ { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) = ∅ )
26 21 24 25 mp3an12 ⊢ ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ≠ ∅ → ∃ 𝑚 ∈ { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) = ∅ )
27 nfv ⊢ Ⅎ 𝑥 𝑚 ∈ ω
28 nfcv ⊢ Ⅎ 𝑥 𝑚
29 4 28 nfin ⊢ Ⅎ 𝑥 ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 )
30 29 nfeq1 ⊢ Ⅎ 𝑥 ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) = ∅
31 27 30 nfan ⊢ Ⅎ 𝑥 ( 𝑚 ∈ ω ∧ ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) = ∅ )
32 simprr ⊢ ( ( ( 𝑚 ∈ ω ∧ ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) = ∅ ) ∧ ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ) → 𝜑 )
33 sspss ⊢ ( 𝑦 ⊆ 𝑥 ↔ ( 𝑦 ⊊ 𝑥 ∨ 𝑦 = 𝑥 ) )
34 rspe ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚 ) → ∃ 𝑚 ∈ ω 𝑥 ≈ 𝑚 )
35 pssss ⊢ ( 𝑦 ⊊ 𝑥 → 𝑦 ⊆ 𝑥 )
36 ssfi ⊢ ( ( 𝑥 ∈ Fin ∧ 𝑦 ⊆ 𝑥 ) → 𝑦 ∈ Fin )
37 35 36 sylan2 ⊢ ( ( 𝑥 ∈ Fin ∧ 𝑦 ⊊ 𝑥 ) → 𝑦 ∈ Fin )
38 37 ex ⊢ ( 𝑥 ∈ Fin → ( 𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin ) )
39 7 38 sylbir ⊢ ( ∃ 𝑚 ∈ ω 𝑥 ≈ 𝑚 → ( 𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin ) )
40 34 39 syl ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚 ) → ( 𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin ) )
41 40 adantrr ⊢ ( ( 𝑚 ∈ ω ∧ ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ) → ( 𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin ) )
42 41 adantrr ⊢ ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) → ( 𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin ) )
43 isfi ⊢ ( 𝑦 ∈ Fin ↔ ∃ 𝑘 ∈ ω 𝑦 ≈ 𝑘 )
44 simprll ⊢ ( ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘 ) ∧ 𝑦 ⊊ 𝑥 ) ) → 𝑘 ∈ ω )
45 simprlr ⊢ ( ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘 ) ∧ 𝑦 ⊊ 𝑥 ) ) → 𝑦 ≈ 𝑘 )
46 simplrr ⊢ ( ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘 ) ∧ 𝑦 ⊊ 𝑥 ) ) → 𝜓 )
47 vex ⊢ 𝑦 ∈ V
48 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≈ 𝑘 ↔ 𝑦 ≈ 𝑘 ) )
49 48 1 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ≈ 𝑘 ∧ 𝜑 ) ↔ ( 𝑦 ≈ 𝑘 ∧ 𝜓 ) ) )
50 47 49 spcev ⊢ ( ( 𝑦 ≈ 𝑘 ∧ 𝜓 ) → ∃ 𝑥 ( 𝑥 ≈ 𝑘 ∧ 𝜑 ) )
51 45 46 50 syl2anc ⊢ ( ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘 ) ∧ 𝑦 ⊊ 𝑥 ) ) → ∃ 𝑥 ( 𝑥 ≈ 𝑘 ∧ 𝜑 ) )
52 34 7 sylibr ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚 ) → 𝑥 ∈ Fin )
53 52 adantrr ⊢ ( ( 𝑚 ∈ ω ∧ ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ) → 𝑥 ∈ Fin )
54 53 adantrr ⊢ ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) → 𝑥 ∈ Fin )
55 54 adantr ⊢ ( ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) ∧ ( 𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘 ) ) → 𝑥 ∈ Fin )
56 php3 ⊢ ( ( 𝑥 ∈ Fin ∧ 𝑦 ⊊ 𝑥 ) → 𝑦 ≺ 𝑥 )
57 56 ex ⊢ ( 𝑥 ∈ Fin → ( 𝑦 ⊊ 𝑥 → 𝑦 ≺ 𝑥 ) )
58 55 57 syl ⊢ ( ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) ∧ ( 𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘 ) ) → ( 𝑦 ⊊ 𝑥 → 𝑦 ≺ 𝑥 ) )
59 vex ⊢ 𝑘 ∈ V
60 ssdomg ⊢ ( 𝑘 ∈ V → ( 𝑚 ⊆ 𝑘 → 𝑚 ≼ 𝑘 ) )
61 59 60 ax-mp ⊢ ( 𝑚 ⊆ 𝑘 → 𝑚 ≼ 𝑘 )
62 endomtr ⊢ ( ( 𝑥 ≈ 𝑚 ∧ 𝑚 ≼ 𝑘 ) → 𝑥 ≼ 𝑘 )
63 62 ex ⊢ ( 𝑥 ≈ 𝑚 → ( 𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑘 ) )
64 63 ad2antrr ⊢ ( ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) → ( 𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑘 ) )
65 64 ad2antlr ⊢ ( ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) ∧ ( 𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘 ) ) → ( 𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑘 ) )
66 ensym ⊢ ( 𝑦 ≈ 𝑘 → 𝑘 ≈ 𝑦 )
67 domentr ⊢ ( ( 𝑥 ≼ 𝑘 ∧ 𝑘 ≈ 𝑦 ) → 𝑥 ≼ 𝑦 )
68 66 67 sylan2 ⊢ ( ( 𝑥 ≼ 𝑘 ∧ 𝑦 ≈ 𝑘 ) → 𝑥 ≼ 𝑦 )
69 68 expcom ⊢ ( 𝑦 ≈ 𝑘 → ( 𝑥 ≼ 𝑘 → 𝑥 ≼ 𝑦 ) )
70 69 ad2antll ⊢ ( ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) ∧ ( 𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘 ) ) → ( 𝑥 ≼ 𝑘 → 𝑥 ≼ 𝑦 ) )
71 65 70 syld ⊢ ( ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) ∧ ( 𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘 ) ) → ( 𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑦 ) )
72 61 71 syl5 ⊢ ( ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) ∧ ( 𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘 ) ) → ( 𝑚 ⊆ 𝑘 → 𝑥 ≼ 𝑦 ) )
73 domnsym ⊢ ( 𝑥 ≼ 𝑦 → ¬ 𝑦 ≺ 𝑥 )
74 73 con2i ⊢ ( 𝑦 ≺ 𝑥 → ¬ 𝑥 ≼ 𝑦 )
75 72 74 nsyli ⊢ ( ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) ∧ ( 𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘 ) ) → ( 𝑦 ≺ 𝑥 → ¬ 𝑚 ⊆ 𝑘 ) )
76 58 75 syld ⊢ ( ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) ∧ ( 𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘 ) ) → ( 𝑦 ⊊ 𝑥 → ¬ 𝑚 ⊆ 𝑘 ) )
77 76 impr ⊢ ( ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘 ) ∧ 𝑦 ⊊ 𝑥 ) ) → ¬ 𝑚 ⊆ 𝑘 )
78 nnord ⊢ ( 𝑚 ∈ ω → Ord 𝑚 )
79 78 ad2antrr ⊢ ( ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘 ) ∧ 𝑦 ⊊ 𝑥 ) ) → Ord 𝑚 )
80 nnord ⊢ ( 𝑘 ∈ ω → Ord 𝑘 )
81 80 adantr ⊢ ( ( 𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘 ) → Ord 𝑘 )
82 81 ad2antrl ⊢ ( ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘 ) ∧ 𝑦 ⊊ 𝑥 ) ) → Ord 𝑘 )
83 ordtri1 ⊢ ( ( Ord 𝑚 ∧ Ord 𝑘 ) → ( 𝑚 ⊆ 𝑘 ↔ ¬ 𝑘 ∈ 𝑚 ) )
84 83 con2bid ⊢ ( ( Ord 𝑚 ∧ Ord 𝑘 ) → ( 𝑘 ∈ 𝑚 ↔ ¬ 𝑚 ⊆ 𝑘 ) )
85 79 82 84 syl2anc ⊢ ( ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘 ) ∧ 𝑦 ⊊ 𝑥 ) ) → ( 𝑘 ∈ 𝑚 ↔ ¬ 𝑚 ⊆ 𝑘 ) )
86 77 85 mpbird ⊢ ( ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘 ) ∧ 𝑦 ⊊ 𝑥 ) ) → 𝑘 ∈ 𝑚 )
87 44 51 86 jca31 ⊢ ( ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘 ) ∧ 𝑦 ⊊ 𝑥 ) ) → ( ( 𝑘 ∈ ω ∧ ∃ 𝑥 ( 𝑥 ≈ 𝑘 ∧ 𝜑 ) ) ∧ 𝑘 ∈ 𝑚 ) )
88 elin ⊢ ( 𝑘 ∈ ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) ↔ ( 𝑘 ∈ { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∧ 𝑘 ∈ 𝑚 ) )
89 breq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑥 ≈ 𝑛 ↔ 𝑥 ≈ 𝑘 ) )
90 89 anbi1d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) ↔ ( 𝑥 ≈ 𝑘 ∧ 𝜑 ) ) )
91 90 exbidv ⊢ ( 𝑛 = 𝑘 → ( ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ≈ 𝑘 ∧ 𝜑 ) ) )
92 91 elrab ⊢ ( 𝑘 ∈ { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ↔ ( 𝑘 ∈ ω ∧ ∃ 𝑥 ( 𝑥 ≈ 𝑘 ∧ 𝜑 ) ) )
93 92 anbi1i ⊢ ( ( 𝑘 ∈ { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∧ 𝑘 ∈ 𝑚 ) ↔ ( ( 𝑘 ∈ ω ∧ ∃ 𝑥 ( 𝑥 ≈ 𝑘 ∧ 𝜑 ) ) ∧ 𝑘 ∈ 𝑚 ) )
94 88 93 bitri ⊢ ( 𝑘 ∈ ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) ↔ ( ( 𝑘 ∈ ω ∧ ∃ 𝑥 ( 𝑥 ≈ 𝑘 ∧ 𝜑 ) ) ∧ 𝑘 ∈ 𝑚 ) )
95 87 94 sylibr ⊢ ( ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘 ) ∧ 𝑦 ⊊ 𝑥 ) ) → 𝑘 ∈ ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) )
96 95 ne0d ⊢ ( ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘 ) ∧ 𝑦 ⊊ 𝑥 ) ) → ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) ≠ ∅ )
97 96 exp44 ⊢ ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) → ( 𝑘 ∈ ω → ( 𝑦 ≈ 𝑘 → ( 𝑦 ⊊ 𝑥 → ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) ≠ ∅ ) ) ) )
98 97 rexlimdv ⊢ ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) → ( ∃ 𝑘 ∈ ω 𝑦 ≈ 𝑘 → ( 𝑦 ⊊ 𝑥 → ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) ≠ ∅ ) ) )
99 43 98 syl5bi ⊢ ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) → ( 𝑦 ∈ Fin → ( 𝑦 ⊊ 𝑥 → ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) ≠ ∅ ) ) )
100 99 com23 ⊢ ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) → ( 𝑦 ⊊ 𝑥 → ( 𝑦 ∈ Fin → ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) ≠ ∅ ) ) )
101 42 100 mpdd ⊢ ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) → ( 𝑦 ⊊ 𝑥 → ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) ≠ ∅ ) )
102 101 necon2bd ⊢ ( ( 𝑚 ∈ ω ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) → ( ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) = ∅ → ¬ 𝑦 ⊊ 𝑥 ) )
103 102 ex ⊢ ( 𝑚 ∈ ω → ( ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) → ( ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) = ∅ → ¬ 𝑦 ⊊ 𝑥 ) ) )
104 103 com23 ⊢ ( 𝑚 ∈ ω → ( ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) = ∅ → ( ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) → ¬ 𝑦 ⊊ 𝑥 ) ) )
105 104 imp31 ⊢ ( ( ( 𝑚 ∈ ω ∧ ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) = ∅ ) ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) → ¬ 𝑦 ⊊ 𝑥 )
106 105 pm2.21d ⊢ ( ( ( 𝑚 ∈ ω ∧ ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) = ∅ ) ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) → ( 𝑦 ⊊ 𝑥 → 𝑥 = 𝑦 ) )
107 equcomi ⊢ ( 𝑦 = 𝑥 → 𝑥 = 𝑦 )
108 107 a1i ⊢ ( ( ( 𝑚 ∈ ω ∧ ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) = ∅ ) ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) → ( 𝑦 = 𝑥 → 𝑥 = 𝑦 ) )
109 106 108 jaod ⊢ ( ( ( 𝑚 ∈ ω ∧ ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) = ∅ ) ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) → ( ( 𝑦 ⊊ 𝑥 ∨ 𝑦 = 𝑥 ) → 𝑥 = 𝑦 ) )
110 33 109 syl5bi ⊢ ( ( ( 𝑚 ∈ ω ∧ ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) = ∅ ) ∧ ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ∧ 𝜓 ) ) → ( 𝑦 ⊆ 𝑥 → 𝑥 = 𝑦 ) )
111 110 expr ⊢ ( ( ( 𝑚 ∈ ω ∧ ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) = ∅ ) ∧ ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ) → ( 𝜓 → ( 𝑦 ⊆ 𝑥 → 𝑥 = 𝑦 ) ) )
112 111 com23 ⊢ ( ( ( 𝑚 ∈ ω ∧ ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) = ∅ ) ∧ ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ) → ( 𝑦 ⊆ 𝑥 → ( 𝜓 → 𝑥 = 𝑦 ) ) )
113 112 impd ⊢ ( ( ( 𝑚 ∈ ω ∧ ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) = ∅ ) ∧ ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ) → ( ( 𝑦 ⊆ 𝑥 ∧ 𝜓 ) → 𝑥 = 𝑦 ) )
114 113 alrimiv ⊢ ( ( ( 𝑚 ∈ ω ∧ ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) = ∅ ) ∧ ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ) → ∀ 𝑦 ( ( 𝑦 ⊆ 𝑥 ∧ 𝜓 ) → 𝑥 = 𝑦 ) )
115 32 114 jca ⊢ ( ( ( 𝑚 ∈ ω ∧ ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) = ∅ ) ∧ ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ) → ( 𝜑 ∧ ∀ 𝑦 ( ( 𝑦 ⊆ 𝑥 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) )
116 115 ex ⊢ ( ( 𝑚 ∈ ω ∧ ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) = ∅ ) → ( ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) → ( 𝜑 ∧ ∀ 𝑦 ( ( 𝑦 ⊆ 𝑥 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) ) )
117 31 116 eximd ⊢ ( ( 𝑚 ∈ ω ∧ ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) = ∅ ) → ( ∃ 𝑥 ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) → ∃ 𝑥 ( 𝜑 ∧ ∀ 𝑦 ( ( 𝑦 ⊆ 𝑥 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) ) )
118 117 impancom ⊢ ( ( 𝑚 ∈ ω ∧ ∃ 𝑥 ( 𝑥 ≈ 𝑚 ∧ 𝜑 ) ) → ( ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) = ∅ → ∃ 𝑥 ( 𝜑 ∧ ∀ 𝑦 ( ( 𝑦 ⊆ 𝑥 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) ) )
119 14 118 sylbi ⊢ ( 𝑚 ∈ { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } → ( ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) = ∅ → ∃ 𝑥 ( 𝜑 ∧ ∀ 𝑦 ( ( 𝑦 ⊆ 𝑥 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) ) )
120 119 rexlimiv ⊢ ( ∃ 𝑚 ∈ { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ( { 𝑛 ∈ ω ∣ ∃ 𝑥 ( 𝑥 ≈ 𝑛 ∧ 𝜑 ) } ∩ 𝑚 ) = ∅ → ∃ 𝑥 ( 𝜑 ∧ ∀ 𝑦 ( ( 𝑦 ⊆ 𝑥 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) )
121 20 26 120 3syl ⊢ ( ∃ 𝑥 ∈ Fin 𝜑 → ∃ 𝑥 ( 𝜑 ∧ ∀ 𝑦 ( ( 𝑦 ⊆ 𝑥 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) )