# Metamath Proof Explorer

## Theorem fin23lem26

Description: Lemma for fin23lem22 . (Contributed by Stefan O'Rear, 1-Nov-2014)

Ref Expression
Assertion fin23lem26 ${⊢}\left(\left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\wedge {i}\in \mathrm{\omega }\right)\to \exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\left({j}\cap {S}\right)\approx {i}$

### Proof

Step Hyp Ref Expression
1 breq2 ${⊢}{i}=\varnothing \to \left(\left({j}\cap {S}\right)\approx {i}↔\left({j}\cap {S}\right)\approx \varnothing \right)$
2 1 rexbidv ${⊢}{i}=\varnothing \to \left(\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\left({j}\cap {S}\right)\approx {i}↔\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\left({j}\cap {S}\right)\approx \varnothing \right)$
3 breq2 ${⊢}{i}={a}\to \left(\left({j}\cap {S}\right)\approx {i}↔\left({j}\cap {S}\right)\approx {a}\right)$
4 3 rexbidv ${⊢}{i}={a}\to \left(\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\left({j}\cap {S}\right)\approx {i}↔\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\left({j}\cap {S}\right)\approx {a}\right)$
5 breq2 ${⊢}{i}=\mathrm{suc}{a}\to \left(\left({j}\cap {S}\right)\approx {i}↔\left({j}\cap {S}\right)\approx \mathrm{suc}{a}\right)$
6 5 rexbidv ${⊢}{i}=\mathrm{suc}{a}\to \left(\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\left({j}\cap {S}\right)\approx {i}↔\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\left({j}\cap {S}\right)\approx \mathrm{suc}{a}\right)$
7 ordom ${⊢}\mathrm{Ord}\mathrm{\omega }$
8 simpl ${⊢}\left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\to {S}\subseteq \mathrm{\omega }$
9 0fin ${⊢}\varnothing \in \mathrm{Fin}$
10 eleq1 ${⊢}{S}=\varnothing \to \left({S}\in \mathrm{Fin}↔\varnothing \in \mathrm{Fin}\right)$
11 9 10 mpbiri ${⊢}{S}=\varnothing \to {S}\in \mathrm{Fin}$
12 11 necon3bi ${⊢}¬{S}\in \mathrm{Fin}\to {S}\ne \varnothing$
13 12 adantl ${⊢}\left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\to {S}\ne \varnothing$
14 tz7.5 ${⊢}\left(\mathrm{Ord}\mathrm{\omega }\wedge {S}\subseteq \mathrm{\omega }\wedge {S}\ne \varnothing \right)\to \exists {j}\in {S}\phantom{\rule{.4em}{0ex}}{S}\cap {j}=\varnothing$
15 7 8 13 14 mp3an2i ${⊢}\left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\to \exists {j}\in {S}\phantom{\rule{.4em}{0ex}}{S}\cap {j}=\varnothing$
16 en0 ${⊢}\left({j}\cap {S}\right)\approx \varnothing ↔{j}\cap {S}=\varnothing$
17 incom ${⊢}{j}\cap {S}={S}\cap {j}$
18 17 eqeq1i ${⊢}{j}\cap {S}=\varnothing ↔{S}\cap {j}=\varnothing$
19 16 18 bitri ${⊢}\left({j}\cap {S}\right)\approx \varnothing ↔{S}\cap {j}=\varnothing$
20 19 rexbii ${⊢}\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\left({j}\cap {S}\right)\approx \varnothing ↔\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}{S}\cap {j}=\varnothing$
21 15 20 sylibr ${⊢}\left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\to \exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\left({j}\cap {S}\right)\approx \varnothing$
22 simplrl ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to {S}\subseteq \mathrm{\omega }$
23 omsson ${⊢}\mathrm{\omega }\subseteq \mathrm{On}$
24 22 23 sstrdi ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to {S}\subseteq \mathrm{On}$
25 24 ssdifssd ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to {S}\setminus \mathrm{suc}{j}\subseteq \mathrm{On}$
26 simplr ${⊢}\left(\left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\wedge {j}\in {S}\right)\to ¬{S}\in \mathrm{Fin}$
27 ssel2 ${⊢}\left({S}\subseteq \mathrm{\omega }\wedge {j}\in {S}\right)\to {j}\in \mathrm{\omega }$
28 onfin2 ${⊢}\mathrm{\omega }=\mathrm{On}\cap \mathrm{Fin}$
29 inss2 ${⊢}\mathrm{On}\cap \mathrm{Fin}\subseteq \mathrm{Fin}$
30 28 29 eqsstri ${⊢}\mathrm{\omega }\subseteq \mathrm{Fin}$
31 peano2 ${⊢}{j}\in \mathrm{\omega }\to \mathrm{suc}{j}\in \mathrm{\omega }$
32 30 31 sseldi ${⊢}{j}\in \mathrm{\omega }\to \mathrm{suc}{j}\in \mathrm{Fin}$
33 27 32 syl ${⊢}\left({S}\subseteq \mathrm{\omega }\wedge {j}\in {S}\right)\to \mathrm{suc}{j}\in \mathrm{Fin}$
34 33 adantlr ${⊢}\left(\left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\wedge {j}\in {S}\right)\to \mathrm{suc}{j}\in \mathrm{Fin}$
35 ssfi ${⊢}\left(\mathrm{suc}{j}\in \mathrm{Fin}\wedge {S}\subseteq \mathrm{suc}{j}\right)\to {S}\in \mathrm{Fin}$
36 35 ex ${⊢}\mathrm{suc}{j}\in \mathrm{Fin}\to \left({S}\subseteq \mathrm{suc}{j}\to {S}\in \mathrm{Fin}\right)$
37 34 36 syl ${⊢}\left(\left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\wedge {j}\in {S}\right)\to \left({S}\subseteq \mathrm{suc}{j}\to {S}\in \mathrm{Fin}\right)$
38 26 37 mtod ${⊢}\left(\left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\wedge {j}\in {S}\right)\to ¬{S}\subseteq \mathrm{suc}{j}$
39 ssdif0 ${⊢}{S}\subseteq \mathrm{suc}{j}↔{S}\setminus \mathrm{suc}{j}=\varnothing$
40 39 necon3bbii ${⊢}¬{S}\subseteq \mathrm{suc}{j}↔{S}\setminus \mathrm{suc}{j}\ne \varnothing$
41 38 40 sylib ${⊢}\left(\left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\wedge {j}\in {S}\right)\to {S}\setminus \mathrm{suc}{j}\ne \varnothing$
42 41 ad2ant2lr ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to {S}\setminus \mathrm{suc}{j}\ne \varnothing$
43 onint ${⊢}\left({S}\setminus \mathrm{suc}{j}\subseteq \mathrm{On}\wedge {S}\setminus \mathrm{suc}{j}\ne \varnothing \right)\to \bigcap \left({S}\setminus \mathrm{suc}{j}\right)\in \left({S}\setminus \mathrm{suc}{j}\right)$
44 25 42 43 syl2anc ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to \bigcap \left({S}\setminus \mathrm{suc}{j}\right)\in \left({S}\setminus \mathrm{suc}{j}\right)$
45 44 eldifad ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to \bigcap \left({S}\setminus \mathrm{suc}{j}\right)\in {S}$
46 simprr ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to \left({j}\cap {S}\right)\approx {a}$
47 en2sn ${⊢}\left({j}\in \mathrm{V}\wedge {a}\in \mathrm{V}\right)\to \left\{{j}\right\}\approx \left\{{a}\right\}$
48 47 el2v ${⊢}\left\{{j}\right\}\approx \left\{{a}\right\}$
49 48 a1i ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to \left\{{j}\right\}\approx \left\{{a}\right\}$
50 simprl ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to {j}\in {S}$
51 22 50 sseldd ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to {j}\in \mathrm{\omega }$
52 nnord ${⊢}{j}\in \mathrm{\omega }\to \mathrm{Ord}{j}$
53 51 52 syl ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to \mathrm{Ord}{j}$
54 ordirr ${⊢}\mathrm{Ord}{j}\to ¬{j}\in {j}$
55 elinel1 ${⊢}{j}\in \left({j}\cap {S}\right)\to {j}\in {j}$
56 54 55 nsyl ${⊢}\mathrm{Ord}{j}\to ¬{j}\in \left({j}\cap {S}\right)$
57 disjsn ${⊢}\left({j}\cap {S}\right)\cap \left\{{j}\right\}=\varnothing ↔¬{j}\in \left({j}\cap {S}\right)$
58 56 57 sylibr ${⊢}\mathrm{Ord}{j}\to \left({j}\cap {S}\right)\cap \left\{{j}\right\}=\varnothing$
59 53 58 syl ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to \left({j}\cap {S}\right)\cap \left\{{j}\right\}=\varnothing$
60 nnord ${⊢}{a}\in \mathrm{\omega }\to \mathrm{Ord}{a}$
61 ordirr ${⊢}\mathrm{Ord}{a}\to ¬{a}\in {a}$
62 60 61 syl ${⊢}{a}\in \mathrm{\omega }\to ¬{a}\in {a}$
63 disjsn ${⊢}{a}\cap \left\{{a}\right\}=\varnothing ↔¬{a}\in {a}$
64 62 63 sylibr ${⊢}{a}\in \mathrm{\omega }\to {a}\cap \left\{{a}\right\}=\varnothing$
65 64 ad2antrr ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to {a}\cap \left\{{a}\right\}=\varnothing$
66 unen ${⊢}\left(\left(\left({j}\cap {S}\right)\approx {a}\wedge \left\{{j}\right\}\approx \left\{{a}\right\}\right)\wedge \left(\left({j}\cap {S}\right)\cap \left\{{j}\right\}=\varnothing \wedge {a}\cap \left\{{a}\right\}=\varnothing \right)\right)\to \left(\left({j}\cap {S}\right)\cup \left\{{j}\right\}\right)\approx \left({a}\cup \left\{{a}\right\}\right)$
67 46 49 59 65 66 syl22anc ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to \left(\left({j}\cap {S}\right)\cup \left\{{j}\right\}\right)\approx \left({a}\cup \left\{{a}\right\}\right)$
68 simprr ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left(\left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\wedge {b}\in {S}\right)\right)\to {b}\in {S}$
69 simplrl ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left(\left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\wedge {b}\in {S}\right)\right)\to {S}\subseteq \mathrm{\omega }$
70 69 23 sstrdi ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left(\left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\wedge {b}\in {S}\right)\right)\to {S}\subseteq \mathrm{On}$
71 ordsuc ${⊢}\mathrm{Ord}{j}↔\mathrm{Ord}\mathrm{suc}{j}$
72 53 71 sylib ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to \mathrm{Ord}\mathrm{suc}{j}$
73 72 adantrr ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left(\left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\wedge {b}\in {S}\right)\right)\to \mathrm{Ord}\mathrm{suc}{j}$
74 simp2 ${⊢}\left({b}\in {S}\wedge {S}\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{suc}{j}\right)\to {S}\subseteq \mathrm{On}$
75 74 ssdifssd ${⊢}\left({b}\in {S}\wedge {S}\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{suc}{j}\right)\to {S}\setminus \mathrm{suc}{j}\subseteq \mathrm{On}$
76 simpl1 ${⊢}\left(\left({b}\in {S}\wedge {S}\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{suc}{j}\right)\wedge ¬{b}\in \mathrm{suc}{j}\right)\to {b}\in {S}$
77 simpr ${⊢}\left(\left({b}\in {S}\wedge {S}\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{suc}{j}\right)\wedge ¬{b}\in \mathrm{suc}{j}\right)\to ¬{b}\in \mathrm{suc}{j}$
78 76 77 eldifd ${⊢}\left(\left({b}\in {S}\wedge {S}\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{suc}{j}\right)\wedge ¬{b}\in \mathrm{suc}{j}\right)\to {b}\in \left({S}\setminus \mathrm{suc}{j}\right)$
79 78 ex ${⊢}\left({b}\in {S}\wedge {S}\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{suc}{j}\right)\to \left(¬{b}\in \mathrm{suc}{j}\to {b}\in \left({S}\setminus \mathrm{suc}{j}\right)\right)$
80 onnmin ${⊢}\left({S}\setminus \mathrm{suc}{j}\subseteq \mathrm{On}\wedge {b}\in \left({S}\setminus \mathrm{suc}{j}\right)\right)\to ¬{b}\in \bigcap \left({S}\setminus \mathrm{suc}{j}\right)$
81 75 79 80 syl6an ${⊢}\left({b}\in {S}\wedge {S}\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{suc}{j}\right)\to \left(¬{b}\in \mathrm{suc}{j}\to ¬{b}\in \bigcap \left({S}\setminus \mathrm{suc}{j}\right)\right)$
82 81 con4d ${⊢}\left({b}\in {S}\wedge {S}\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{suc}{j}\right)\to \left({b}\in \bigcap \left({S}\setminus \mathrm{suc}{j}\right)\to {b}\in \mathrm{suc}{j}\right)$
83 82 imp ${⊢}\left(\left({b}\in {S}\wedge {S}\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{suc}{j}\right)\wedge {b}\in \bigcap \left({S}\setminus \mathrm{suc}{j}\right)\right)\to {b}\in \mathrm{suc}{j}$
84 simp3 ${⊢}\left({b}\in {S}\wedge {S}\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{suc}{j}\right)\to \mathrm{Ord}\mathrm{suc}{j}$
85 ordsucss ${⊢}\mathrm{Ord}\mathrm{suc}{j}\to \left({b}\in \mathrm{suc}{j}\to \mathrm{suc}{b}\subseteq \mathrm{suc}{j}\right)$
86 84 85 syl ${⊢}\left({b}\in {S}\wedge {S}\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{suc}{j}\right)\to \left({b}\in \mathrm{suc}{j}\to \mathrm{suc}{b}\subseteq \mathrm{suc}{j}\right)$
87 86 imp ${⊢}\left(\left({b}\in {S}\wedge {S}\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{suc}{j}\right)\wedge {b}\in \mathrm{suc}{j}\right)\to \mathrm{suc}{b}\subseteq \mathrm{suc}{j}$
88 87 sscond ${⊢}\left(\left({b}\in {S}\wedge {S}\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{suc}{j}\right)\wedge {b}\in \mathrm{suc}{j}\right)\to {S}\setminus \mathrm{suc}{j}\subseteq {S}\setminus \mathrm{suc}{b}$
89 intss ${⊢}{S}\setminus \mathrm{suc}{j}\subseteq {S}\setminus \mathrm{suc}{b}\to \bigcap \left({S}\setminus \mathrm{suc}{b}\right)\subseteq \bigcap \left({S}\setminus \mathrm{suc}{j}\right)$
90 88 89 syl ${⊢}\left(\left({b}\in {S}\wedge {S}\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{suc}{j}\right)\wedge {b}\in \mathrm{suc}{j}\right)\to \bigcap \left({S}\setminus \mathrm{suc}{b}\right)\subseteq \bigcap \left({S}\setminus \mathrm{suc}{j}\right)$
91 simpl2 ${⊢}\left(\left({b}\in {S}\wedge {S}\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{suc}{j}\right)\wedge {b}\in \mathrm{suc}{j}\right)\to {S}\subseteq \mathrm{On}$
92 ordelon ${⊢}\left(\mathrm{Ord}\mathrm{suc}{j}\wedge {b}\in \mathrm{suc}{j}\right)\to {b}\in \mathrm{On}$
93 84 92 sylan ${⊢}\left(\left({b}\in {S}\wedge {S}\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{suc}{j}\right)\wedge {b}\in \mathrm{suc}{j}\right)\to {b}\in \mathrm{On}$
94 onmindif ${⊢}\left({S}\subseteq \mathrm{On}\wedge {b}\in \mathrm{On}\right)\to {b}\in \bigcap \left({S}\setminus \mathrm{suc}{b}\right)$
95 91 93 94 syl2anc ${⊢}\left(\left({b}\in {S}\wedge {S}\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{suc}{j}\right)\wedge {b}\in \mathrm{suc}{j}\right)\to {b}\in \bigcap \left({S}\setminus \mathrm{suc}{b}\right)$
96 90 95 sseldd ${⊢}\left(\left({b}\in {S}\wedge {S}\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{suc}{j}\right)\wedge {b}\in \mathrm{suc}{j}\right)\to {b}\in \bigcap \left({S}\setminus \mathrm{suc}{j}\right)$
97 83 96 impbida ${⊢}\left({b}\in {S}\wedge {S}\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{suc}{j}\right)\to \left({b}\in \bigcap \left({S}\setminus \mathrm{suc}{j}\right)↔{b}\in \mathrm{suc}{j}\right)$
98 68 70 73 97 syl3anc ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left(\left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\wedge {b}\in {S}\right)\right)\to \left({b}\in \bigcap \left({S}\setminus \mathrm{suc}{j}\right)↔{b}\in \mathrm{suc}{j}\right)$
99 df-suc ${⊢}\mathrm{suc}{j}={j}\cup \left\{{j}\right\}$
100 99 eleq2i ${⊢}{b}\in \mathrm{suc}{j}↔{b}\in \left({j}\cup \left\{{j}\right\}\right)$
101 98 100 syl6bb ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left(\left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\wedge {b}\in {S}\right)\right)\to \left({b}\in \bigcap \left({S}\setminus \mathrm{suc}{j}\right)↔{b}\in \left({j}\cup \left\{{j}\right\}\right)\right)$
102 101 expr ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to \left({b}\in {S}\to \left({b}\in \bigcap \left({S}\setminus \mathrm{suc}{j}\right)↔{b}\in \left({j}\cup \left\{{j}\right\}\right)\right)\right)$
103 102 pm5.32rd ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to \left(\left({b}\in \bigcap \left({S}\setminus \mathrm{suc}{j}\right)\wedge {b}\in {S}\right)↔\left({b}\in \left({j}\cup \left\{{j}\right\}\right)\wedge {b}\in {S}\right)\right)$
104 elin ${⊢}{b}\in \left(\bigcap \left({S}\setminus \mathrm{suc}{j}\right)\cap {S}\right)↔\left({b}\in \bigcap \left({S}\setminus \mathrm{suc}{j}\right)\wedge {b}\in {S}\right)$
105 elin ${⊢}{b}\in \left(\left({j}\cup \left\{{j}\right\}\right)\cap {S}\right)↔\left({b}\in \left({j}\cup \left\{{j}\right\}\right)\wedge {b}\in {S}\right)$
106 103 104 105 3bitr4g ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to \left({b}\in \left(\bigcap \left({S}\setminus \mathrm{suc}{j}\right)\cap {S}\right)↔{b}\in \left(\left({j}\cup \left\{{j}\right\}\right)\cap {S}\right)\right)$
107 106 eqrdv ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to \bigcap \left({S}\setminus \mathrm{suc}{j}\right)\cap {S}=\left({j}\cup \left\{{j}\right\}\right)\cap {S}$
108 indir ${⊢}\left({j}\cup \left\{{j}\right\}\right)\cap {S}=\left({j}\cap {S}\right)\cup \left(\left\{{j}\right\}\cap {S}\right)$
109 107 108 syl6eq ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to \bigcap \left({S}\setminus \mathrm{suc}{j}\right)\cap {S}=\left({j}\cap {S}\right)\cup \left(\left\{{j}\right\}\cap {S}\right)$
110 snssi ${⊢}{j}\in {S}\to \left\{{j}\right\}\subseteq {S}$
111 df-ss ${⊢}\left\{{j}\right\}\subseteq {S}↔\left\{{j}\right\}\cap {S}=\left\{{j}\right\}$
112 110 111 sylib ${⊢}{j}\in {S}\to \left\{{j}\right\}\cap {S}=\left\{{j}\right\}$
113 112 uneq2d ${⊢}{j}\in {S}\to \left({j}\cap {S}\right)\cup \left(\left\{{j}\right\}\cap {S}\right)=\left({j}\cap {S}\right)\cup \left\{{j}\right\}$
114 113 ad2antrl ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to \left({j}\cap {S}\right)\cup \left(\left\{{j}\right\}\cap {S}\right)=\left({j}\cap {S}\right)\cup \left\{{j}\right\}$
115 109 114 eqtrd ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to \bigcap \left({S}\setminus \mathrm{suc}{j}\right)\cap {S}=\left({j}\cap {S}\right)\cup \left\{{j}\right\}$
116 df-suc ${⊢}\mathrm{suc}{a}={a}\cup \left\{{a}\right\}$
117 116 a1i ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to \mathrm{suc}{a}={a}\cup \left\{{a}\right\}$
118 67 115 117 3brtr4d ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to \left(\bigcap \left({S}\setminus \mathrm{suc}{j}\right)\cap {S}\right)\approx \mathrm{suc}{a}$
119 ineq1 ${⊢}{b}=\bigcap \left({S}\setminus \mathrm{suc}{j}\right)\to {b}\cap {S}=\bigcap \left({S}\setminus \mathrm{suc}{j}\right)\cap {S}$
120 119 breq1d ${⊢}{b}=\bigcap \left({S}\setminus \mathrm{suc}{j}\right)\to \left(\left({b}\cap {S}\right)\approx \mathrm{suc}{a}↔\left(\bigcap \left({S}\setminus \mathrm{suc}{j}\right)\cap {S}\right)\approx \mathrm{suc}{a}\right)$
121 120 rspcev ${⊢}\left(\bigcap \left({S}\setminus \mathrm{suc}{j}\right)\in {S}\wedge \left(\bigcap \left({S}\setminus \mathrm{suc}{j}\right)\cap {S}\right)\approx \mathrm{suc}{a}\right)\to \exists {b}\in {S}\phantom{\rule{.4em}{0ex}}\left({b}\cap {S}\right)\approx \mathrm{suc}{a}$
122 45 118 121 syl2anc ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\wedge \left({j}\in {S}\wedge \left({j}\cap {S}\right)\approx {a}\right)\right)\to \exists {b}\in {S}\phantom{\rule{.4em}{0ex}}\left({b}\cap {S}\right)\approx \mathrm{suc}{a}$
123 122 rexlimdvaa ${⊢}\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\to \left(\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\left({j}\cap {S}\right)\approx {a}\to \exists {b}\in {S}\phantom{\rule{.4em}{0ex}}\left({b}\cap {S}\right)\approx \mathrm{suc}{a}\right)$
124 ineq1 ${⊢}{b}={j}\to {b}\cap {S}={j}\cap {S}$
125 124 breq1d ${⊢}{b}={j}\to \left(\left({b}\cap {S}\right)\approx \mathrm{suc}{a}↔\left({j}\cap {S}\right)\approx \mathrm{suc}{a}\right)$
126 125 cbvrexvw ${⊢}\exists {b}\in {S}\phantom{\rule{.4em}{0ex}}\left({b}\cap {S}\right)\approx \mathrm{suc}{a}↔\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\left({j}\cap {S}\right)\approx \mathrm{suc}{a}$
127 123 126 syl6ib ${⊢}\left({a}\in \mathrm{\omega }\wedge \left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\right)\to \left(\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\left({j}\cap {S}\right)\approx {a}\to \exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\left({j}\cap {S}\right)\approx \mathrm{suc}{a}\right)$
128 127 ex ${⊢}{a}\in \mathrm{\omega }\to \left(\left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\to \left(\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\left({j}\cap {S}\right)\approx {a}\to \exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\left({j}\cap {S}\right)\approx \mathrm{suc}{a}\right)\right)$
129 2 4 6 21 128 finds2 ${⊢}{i}\in \mathrm{\omega }\to \left(\left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\to \exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\left({j}\cap {S}\right)\approx {i}\right)$
130 129 impcom ${⊢}\left(\left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\wedge {i}\in \mathrm{\omega }\right)\to \exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\left({j}\cap {S}\right)\approx {i}$