Metamath Proof Explorer

Theorem salexct

Description: An example of nontrivial sigma-algebra: the collection of all subsets which either are countable or have countable complement. (Contributed by Glauco Siliprandi, 3-Jan-2021)

Ref Expression
Hypotheses salexct.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
salexct.b ⊢ 𝑆 = { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑥 ≼ ω ∨ ( 𝐴 ∖ 𝑥 ) ≼ ω ) }
Assertion salexct ( 𝜑 → 𝑆 ∈ SAlg )

Proof

Step Hyp Ref Expression
1 salexct.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 salexct.b ⊢ 𝑆 = { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑥 ≼ ω ∨ ( 𝐴 ∖ 𝑥 ) ≼ ω ) }
3 1 pwexd ⊢ ( 𝜑 → 𝒫 𝐴 ∈ V )
4 rabexg ⊢ ( 𝒫 𝐴 ∈ V → { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑥 ≼ ω ∨ ( 𝐴 ∖ 𝑥 ) ≼ ω ) } ∈ V )
5 3 4 syl ⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑥 ≼ ω ∨ ( 𝐴 ∖ 𝑥 ) ≼ ω ) } ∈ V )
6 2 5 eqeltrid ⊢ ( 𝜑 → 𝑆 ∈ V )
7 0elpw ⊢ ∅ ∈ 𝒫 𝐴
8 7 a1i ⊢ ( 𝜑 → ∅ ∈ 𝒫 𝐴 )
9 0fi ⊢ ∅ ∈ Fin
10 fict ⊢ ( ∅ ∈ Fin → ∅ ≼ ω )
11 9 10 ax-mp ⊢ ∅ ≼ ω
12 11 orci ⊢ ( ∅ ≼ ω ∨ ( 𝐴 ∖ ∅ ) ≼ ω )
13 12 a1i ⊢ ( 𝜑 → ( ∅ ≼ ω ∨ ( 𝐴 ∖ ∅ ) ≼ ω ) )
14 8 13 jca ⊢ ( 𝜑 → ( ∅ ∈ 𝒫 𝐴 ∧ ( ∅ ≼ ω ∨ ( 𝐴 ∖ ∅ ) ≼ ω ) ) )
15 breq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ≼ ω ↔ ∅ ≼ ω ) )
16 difeq2 ⊢ ( 𝑥 = ∅ → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ ∅ ) )
17 16 breq1d ⊢ ( 𝑥 = ∅ → ( ( 𝐴 ∖ 𝑥 ) ≼ ω ↔ ( 𝐴 ∖ ∅ ) ≼ ω ) )
18 15 17 orbi12d ⊢ ( 𝑥 = ∅ → ( ( 𝑥 ≼ ω ∨ ( 𝐴 ∖ 𝑥 ) ≼ ω ) ↔ ( ∅ ≼ ω ∨ ( 𝐴 ∖ ∅ ) ≼ ω ) ) )
19 18 2 elrab2 ⊢ ( ∅ ∈ 𝑆 ↔ ( ∅ ∈ 𝒫 𝐴 ∧ ( ∅ ≼ ω ∨ ( 𝐴 ∖ ∅ ) ≼ ω ) ) )
20 14 19 sylibr ⊢ ( 𝜑 → ∅ ∈ 𝑆 )
21 snidg ⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ { 𝑦 } )
22 snelpwi ⊢ ( 𝑦 ∈ 𝐴 → { 𝑦 } ∈ 𝒫 𝐴 )
23 snfi ⊢ { 𝑦 } ∈ Fin
24 fict ⊢ ( { 𝑦 } ∈ Fin → { 𝑦 } ≼ ω )
25 23 24 ax-mp ⊢ { 𝑦 } ≼ ω
26 25 orci ⊢ ( { 𝑦 } ≼ ω ∨ ( 𝐴 ∖ { 𝑦 } ) ≼ ω )
27 26 a1i ⊢ ( 𝑦 ∈ 𝐴 → ( { 𝑦 } ≼ ω ∨ ( 𝐴 ∖ { 𝑦 } ) ≼ ω ) )
28 22 27 jca ⊢ ( 𝑦 ∈ 𝐴 → ( { 𝑦 } ∈ 𝒫 𝐴 ∧ ( { 𝑦 } ≼ ω ∨ ( 𝐴 ∖ { 𝑦 } ) ≼ ω ) ) )
29 breq1 ⊢ ( 𝑥 = { 𝑦 } → ( 𝑥 ≼ ω ↔ { 𝑦 } ≼ ω ) )
30 difeq2 ⊢ ( 𝑥 = { 𝑦 } → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ { 𝑦 } ) )
31 30 breq1d ⊢ ( 𝑥 = { 𝑦 } → ( ( 𝐴 ∖ 𝑥 ) ≼ ω ↔ ( 𝐴 ∖ { 𝑦 } ) ≼ ω ) )
32 29 31 orbi12d ⊢ ( 𝑥 = { 𝑦 } → ( ( 𝑥 ≼ ω ∨ ( 𝐴 ∖ 𝑥 ) ≼ ω ) ↔ ( { 𝑦 } ≼ ω ∨ ( 𝐴 ∖ { 𝑦 } ) ≼ ω ) ) )
33 32 2 elrab2 ⊢ ( { 𝑦 } ∈ 𝑆 ↔ ( { 𝑦 } ∈ 𝒫 𝐴 ∧ ( { 𝑦 } ≼ ω ∨ ( 𝐴 ∖ { 𝑦 } ) ≼ ω ) ) )
34 28 33 sylibr ⊢ ( 𝑦 ∈ 𝐴 → { 𝑦 } ∈ 𝑆 )
35 elunii ⊢ ( ( 𝑦 ∈ { 𝑦 } ∧ { 𝑦 } ∈ 𝑆 ) → 𝑦 ∈ ∪ 𝑆 )
36 21 34 35 syl2anc ⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ∪ 𝑆 )
37 36 rgen ⊢ ∀ 𝑦 ∈ 𝐴 𝑦 ∈ ∪ 𝑆
38 dfss3 ⊢ ( 𝐴 ⊆ ∪ 𝑆 ↔ ∀ 𝑦 ∈ 𝐴 𝑦 ∈ ∪ 𝑆 )
39 37 38 mpbir ⊢ 𝐴 ⊆ ∪ 𝑆
40 ssrab2 ⊢ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑥 ≼ ω ∨ ( 𝐴 ∖ 𝑥 ) ≼ ω ) } ⊆ 𝒫 𝐴
41 2 40 eqsstri ⊢ 𝑆 ⊆ 𝒫 𝐴
42 41 unissi ⊢ ∪ 𝑆 ⊆ ∪ 𝒫 𝐴
43 unipw ⊢ ∪ 𝒫 𝐴 = 𝐴
44 42 43 sseqtri ⊢ ∪ 𝑆 ⊆ 𝐴
45 39 44 eqssi ⊢ 𝐴 = ∪ 𝑆
46 difssd ⊢ ( 𝜑 → ( 𝐴 ∖ 𝑥 ) ⊆ 𝐴 )
47 1 46 ssexd ⊢ ( 𝜑 → ( 𝐴 ∖ 𝑥 ) ∈ V )
48 elpwg ⊢ ( ( 𝐴 ∖ 𝑥 ) ∈ V → ( ( 𝐴 ∖ 𝑥 ) ∈ 𝒫 𝐴 ↔ ( 𝐴 ∖ 𝑥 ) ⊆ 𝐴 ) )
49 47 48 syl ⊢ ( 𝜑 → ( ( 𝐴 ∖ 𝑥 ) ∈ 𝒫 𝐴 ↔ ( 𝐴 ∖ 𝑥 ) ⊆ 𝐴 ) )
50 46 49 mpbird ⊢ ( 𝜑 → ( 𝐴 ∖ 𝑥 ) ∈ 𝒫 𝐴 )
51 50 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑥 ≼ ω ) → ( 𝐴 ∖ 𝑥 ) ∈ 𝒫 𝐴 )
52 41 sseli ⊢ ( 𝑥 ∈ 𝑆 → 𝑥 ∈ 𝒫 𝐴 )
53 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴 )
54 52 53 syl ⊢ ( 𝑥 ∈ 𝑆 → 𝑥 ⊆ 𝐴 )
55 dfss4 ⊢ ( 𝑥 ⊆ 𝐴 ↔ ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) = 𝑥 )
56 54 55 sylib ⊢ ( 𝑥 ∈ 𝑆 → ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) = 𝑥 )
57 56 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑥 ≼ ω ) → ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) = 𝑥 )
58 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑥 ≼ ω ) → 𝑥 ≼ ω )
59 57 58 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑥 ≼ ω ) → ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) ≼ ω )
60 olc ⊢ ( ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) ≼ ω → ( ( 𝐴 ∖ 𝑥 ) ≼ ω ∨ ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) ≼ ω ) )
61 59 60 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑥 ≼ ω ) → ( ( 𝐴 ∖ 𝑥 ) ≼ ω ∨ ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) ≼ ω ) )
62 51 61 jca ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑥 ≼ ω ) → ( ( 𝐴 ∖ 𝑥 ) ∈ 𝒫 𝐴 ∧ ( ( 𝐴 ∖ 𝑥 ) ≼ ω ∨ ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) ≼ ω ) ) )
63 breq1 ⊢ ( 𝑦 = ( 𝐴 ∖ 𝑥 ) → ( 𝑦 ≼ ω ↔ ( 𝐴 ∖ 𝑥 ) ≼ ω ) )
64 difeq2 ⊢ ( 𝑦 = ( 𝐴 ∖ 𝑥 ) → ( 𝐴 ∖ 𝑦 ) = ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) )
65 64 breq1d ⊢ ( 𝑦 = ( 𝐴 ∖ 𝑥 ) → ( ( 𝐴 ∖ 𝑦 ) ≼ ω ↔ ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) ≼ ω ) )
66 63 65 orbi12d ⊢ ( 𝑦 = ( 𝐴 ∖ 𝑥 ) → ( ( 𝑦 ≼ ω ∨ ( 𝐴 ∖ 𝑦 ) ≼ ω ) ↔ ( ( 𝐴 ∖ 𝑥 ) ≼ ω ∨ ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) ≼ ω ) ) )
67 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≼ ω ↔ 𝑦 ≼ ω ) )
68 difeq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ 𝑦 ) )
69 68 breq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ∖ 𝑥 ) ≼ ω ↔ ( 𝐴 ∖ 𝑦 ) ≼ ω ) )
70 67 69 orbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ≼ ω ∨ ( 𝐴 ∖ 𝑥 ) ≼ ω ) ↔ ( 𝑦 ≼ ω ∨ ( 𝐴 ∖ 𝑦 ) ≼ ω ) ) )
71 70 cbvrabv ⊢ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑥 ≼ ω ∨ ( 𝐴 ∖ 𝑥 ) ≼ ω ) } = { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑦 ≼ ω ∨ ( 𝐴 ∖ 𝑦 ) ≼ ω ) }
72 2 71 eqtri ⊢ 𝑆 = { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑦 ≼ ω ∨ ( 𝐴 ∖ 𝑦 ) ≼ ω ) }
73 66 72 elrab2 ⊢ ( ( 𝐴 ∖ 𝑥 ) ∈ 𝑆 ↔ ( ( 𝐴 ∖ 𝑥 ) ∈ 𝒫 𝐴 ∧ ( ( 𝐴 ∖ 𝑥 ) ≼ ω ∨ ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) ≼ ω ) ) )
74 62 73 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑥 ≼ ω ) → ( 𝐴 ∖ 𝑥 ) ∈ 𝑆 )
75 50 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ¬ 𝑥 ≼ ω ) → ( 𝐴 ∖ 𝑥 ) ∈ 𝒫 𝐴 )
76 2 reqabi ⊢ ( 𝑥 ∈ 𝑆 ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝑥 ≼ ω ∨ ( 𝐴 ∖ 𝑥 ) ≼ ω ) ) )
77 76 biimpi ⊢ ( 𝑥 ∈ 𝑆 → ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝑥 ≼ ω ∨ ( 𝐴 ∖ 𝑥 ) ≼ ω ) ) )
78 77 simprd ⊢ ( 𝑥 ∈ 𝑆 → ( 𝑥 ≼ ω ∨ ( 𝐴 ∖ 𝑥 ) ≼ ω ) )
79 78 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ≼ ω ∨ ( 𝐴 ∖ 𝑥 ) ≼ ω ) )
80 79 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ¬ 𝑥 ≼ ω ) → ( 𝑥 ≼ ω ∨ ( 𝐴 ∖ 𝑥 ) ≼ ω ) )
81 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ¬ 𝑥 ≼ ω ) → ¬ 𝑥 ≼ ω )
82 pm2.53 ⊢ ( ( 𝑥 ≼ ω ∨ ( 𝐴 ∖ 𝑥 ) ≼ ω ) → ( ¬ 𝑥 ≼ ω → ( 𝐴 ∖ 𝑥 ) ≼ ω ) )
83 80 81 82 sylc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ¬ 𝑥 ≼ ω ) → ( 𝐴 ∖ 𝑥 ) ≼ ω )
84 orc ⊢ ( ( 𝐴 ∖ 𝑥 ) ≼ ω → ( ( 𝐴 ∖ 𝑥 ) ≼ ω ∨ ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) ≼ ω ) )
85 83 84 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ¬ 𝑥 ≼ ω ) → ( ( 𝐴 ∖ 𝑥 ) ≼ ω ∨ ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) ≼ ω ) )
86 75 85 jca ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ¬ 𝑥 ≼ ω ) → ( ( 𝐴 ∖ 𝑥 ) ∈ 𝒫 𝐴 ∧ ( ( 𝐴 ∖ 𝑥 ) ≼ ω ∨ ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) ≼ ω ) ) )
87 86 73 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ¬ 𝑥 ≼ ω ) → ( 𝐴 ∖ 𝑥 ) ∈ 𝑆 )
88 74 87 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐴 ∖ 𝑥 ) ∈ 𝑆 )
89 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝑆 → 𝑥 ⊆ 𝑆 )
90 89 adantr ⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ⊆ 𝑆 )
91 simpr ⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑥 )
92 90 91 sseldd ⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑆 )
93 41 sseli ⊢ ( 𝑦 ∈ 𝑆 → 𝑦 ∈ 𝒫 𝐴 )
94 elpwi ⊢ ( 𝑦 ∈ 𝒫 𝐴 → 𝑦 ⊆ 𝐴 )
95 93 94 syl ⊢ ( 𝑦 ∈ 𝑆 → 𝑦 ⊆ 𝐴 )
96 92 95 syl ⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ⊆ 𝐴 )
97 96 ralrimiva ⊢ ( 𝑥 ∈ 𝒫 𝑆 → ∀ 𝑦 ∈ 𝑥 𝑦 ⊆ 𝐴 )
98 unissb ⊢ ( ∪ 𝑥 ⊆ 𝐴 ↔ ∀ 𝑦 ∈ 𝑥 𝑦 ⊆ 𝐴 )
99 97 98 sylibr ⊢ ( 𝑥 ∈ 𝒫 𝑆 → ∪ 𝑥 ⊆ 𝐴 )
100 vuniex ⊢ ∪ 𝑥 ∈ V
101 100 elpw ⊢ ( ∪ 𝑥 ∈ 𝒫 𝐴 ↔ ∪ 𝑥 ⊆ 𝐴 )
102 99 101 sylibr ⊢ ( 𝑥 ∈ 𝒫 𝑆 → ∪ 𝑥 ∈ 𝒫 𝐴 )
103 102 adantr ⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω ) → ∪ 𝑥 ∈ 𝒫 𝐴 )
104 id ⊢ ( ( 𝑥 ≼ ω ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω ) → ( 𝑥 ≼ ω ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω ) )
105 104 adantll ⊢ ( ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω ) ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω ) → ( 𝑥 ≼ ω ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω ) )
106 unictb ⊢ ( ( 𝑥 ≼ ω ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω ) → ∪ 𝑥 ≼ ω )
107 orc ⊢ ( ∪ 𝑥 ≼ ω → ( ∪ 𝑥 ≼ ω ∨ ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) )
108 105 106 107 3syl ⊢ ( ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω ) ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω ) → ( ∪ 𝑥 ≼ ω ∨ ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) )
109 rexnal ⊢ ( ∃ 𝑦 ∈ 𝑥 ¬ 𝑦 ≼ ω ↔ ¬ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω )
110 109 bilanri ⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω ) → ∃ 𝑦 ∈ 𝑥 ¬ 𝑦 ≼ ω )
111 nfv ⊢ Ⅎ 𝑦 𝑥 ∈ 𝒫 𝑆
112 nfra1 ⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω
113 112 nfn ⊢ Ⅎ 𝑦 ¬ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω
114 111 113 nfan ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω )
115 nfv ⊢ Ⅎ 𝑦 ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω
116 elssuni ⊢ ( 𝑦 ∈ 𝑥 → 𝑦 ⊆ ∪ 𝑥 )
117 116 3ad2ant2 ⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω ) → 𝑦 ⊆ ∪ 𝑥 )
118 117 sscond ⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω ) → ( 𝐴 ∖ ∪ 𝑥 ) ⊆ ( 𝐴 ∖ 𝑦 ) )
119 92 3adant3 ⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω ) → 𝑦 ∈ 𝑆 )
120 simp3 ⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω ) → ¬ 𝑦 ≼ ω )
121 72 reqabi ⊢ ( 𝑦 ∈ 𝑆 ↔ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑦 ≼ ω ∨ ( 𝐴 ∖ 𝑦 ) ≼ ω ) ) )
122 121 biimpi ⊢ ( 𝑦 ∈ 𝑆 → ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑦 ≼ ω ∨ ( 𝐴 ∖ 𝑦 ) ≼ ω ) ) )
123 122 simprd ⊢ ( 𝑦 ∈ 𝑆 → ( 𝑦 ≼ ω ∨ ( 𝐴 ∖ 𝑦 ) ≼ ω ) )
124 123 adantr ⊢ ( ( 𝑦 ∈ 𝑆 ∧ ¬ 𝑦 ≼ ω ) → ( 𝑦 ≼ ω ∨ ( 𝐴 ∖ 𝑦 ) ≼ ω ) )
125 simpr ⊢ ( ( 𝑦 ∈ 𝑆 ∧ ¬ 𝑦 ≼ ω ) → ¬ 𝑦 ≼ ω )
126 pm2.53 ⊢ ( ( 𝑦 ≼ ω ∨ ( 𝐴 ∖ 𝑦 ) ≼ ω ) → ( ¬ 𝑦 ≼ ω → ( 𝐴 ∖ 𝑦 ) ≼ ω ) )
127 124 125 126 sylc ⊢ ( ( 𝑦 ∈ 𝑆 ∧ ¬ 𝑦 ≼ ω ) → ( 𝐴 ∖ 𝑦 ) ≼ ω )
128 119 120 127 syl2anc ⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω ) → ( 𝐴 ∖ 𝑦 ) ≼ ω )
129 ssct ⊢ ( ( ( 𝐴 ∖ ∪ 𝑥 ) ⊆ ( 𝐴 ∖ 𝑦 ) ∧ ( 𝐴 ∖ 𝑦 ) ≼ ω ) → ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω )
130 118 128 129 syl2anc ⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω ) → ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω )
131 130 3exp ⊢ ( 𝑥 ∈ 𝒫 𝑆 → ( 𝑦 ∈ 𝑥 → ( ¬ 𝑦 ≼ ω → ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) ) )
132 131 adantr ⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω ) → ( 𝑦 ∈ 𝑥 → ( ¬ 𝑦 ≼ ω → ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) ) )
133 114 115 132 rexlimd ⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω ) → ( ∃ 𝑦 ∈ 𝑥 ¬ 𝑦 ≼ ω → ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) )
134 110 133 mpd ⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω ) → ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω )
135 olc ⊢ ( ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω → ( ∪ 𝑥 ≼ ω ∨ ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) )
136 134 135 syl ⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω ) → ( ∪ 𝑥 ≼ ω ∨ ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) )
137 136 adantlr ⊢ ( ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω ) ∧ ¬ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω ) → ( ∪ 𝑥 ≼ ω ∨ ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) )
138 108 137 pm2.61dan ⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω ) → ( ∪ 𝑥 ≼ ω ∨ ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) )
139 103 138 jca ⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω ) → ( ∪ 𝑥 ∈ 𝒫 𝐴 ∧ ( ∪ 𝑥 ≼ ω ∨ ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) ) )
140 breq1 ⊢ ( 𝑦 = ∪ 𝑥 → ( 𝑦 ≼ ω ↔ ∪ 𝑥 ≼ ω ) )
141 difeq2 ⊢ ( 𝑦 = ∪ 𝑥 → ( 𝐴 ∖ 𝑦 ) = ( 𝐴 ∖ ∪ 𝑥 ) )
142 141 breq1d ⊢ ( 𝑦 = ∪ 𝑥 → ( ( 𝐴 ∖ 𝑦 ) ≼ ω ↔ ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) )
143 140 142 orbi12d ⊢ ( 𝑦 = ∪ 𝑥 → ( ( 𝑦 ≼ ω ∨ ( 𝐴 ∖ 𝑦 ) ≼ ω ) ↔ ( ∪ 𝑥 ≼ ω ∨ ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) ) )
144 143 72 elrab2 ⊢ ( ∪ 𝑥 ∈ 𝑆 ↔ ( ∪ 𝑥 ∈ 𝒫 𝐴 ∧ ( ∪ 𝑥 ≼ ω ∨ ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) ) )
145 139 144 sylibr ⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω ) → ∪ 𝑥 ∈ 𝑆 )
146 145 3adant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω ) → ∪ 𝑥 ∈ 𝑆 )
147 6 20 45 88 146 issald ⊢ ( 𝜑 → 𝑆 ∈ SAlg )