Metamath Proof Explorer

Theorem fin23lem26

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

Ref Expression
Assertion fin23lem26 ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑖 ∈ ω ) → ∃ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 )

Proof

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