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	bicomi	⊢ ( ¬ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω ↔ ∃ 𝑦 ∈ 𝑥 ¬ 𝑦 ≼ ω )
111	110	biimpi	⊢ ( ¬ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω → ∃ 𝑦 ∈ 𝑥 ¬ 𝑦 ≼ ω )
112	111	adantl	⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω ) → ∃ 𝑦 ∈ 𝑥 ¬ 𝑦 ≼ ω )
113		nfv	⊢ Ⅎ 𝑦 𝑥 ∈ 𝒫 𝑆
114		nfra1	⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω
115	114	nfn	⊢ Ⅎ 𝑦 ¬ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω
116	113 115	nfan	⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω )
117		nfv	⊢ Ⅎ 𝑦 ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω
118		elssuni	⊢ ( 𝑦 ∈ 𝑥 → 𝑦 ⊆ ∪ 𝑥 )
119	118	3ad2ant2	⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω ) → 𝑦 ⊆ ∪ 𝑥 )
120	119	sscond	⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω ) → ( 𝐴 ∖ ∪ 𝑥 ) ⊆ ( 𝐴 ∖ 𝑦 ) )
121	92	3adant3	⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω ) → 𝑦 ∈ 𝑆 )
122		simp3	⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω ) → ¬ 𝑦 ≼ ω )
123	72	reqabi	⊢ ( 𝑦 ∈ 𝑆 ↔ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑦 ≼ ω ∨ ( 𝐴 ∖ 𝑦 ) ≼ ω ) ) )
124	123	biimpi	⊢ ( 𝑦 ∈ 𝑆 → ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑦 ≼ ω ∨ ( 𝐴 ∖ 𝑦 ) ≼ ω ) ) )
125	124	simprd	⊢ ( 𝑦 ∈ 𝑆 → ( 𝑦 ≼ ω ∨ ( 𝐴 ∖ 𝑦 ) ≼ ω ) )
126	125	adantr	⊢ ( ( 𝑦 ∈ 𝑆 ∧ ¬ 𝑦 ≼ ω ) → ( 𝑦 ≼ ω ∨ ( 𝐴 ∖ 𝑦 ) ≼ ω ) )
127		simpr	⊢ ( ( 𝑦 ∈ 𝑆 ∧ ¬ 𝑦 ≼ ω ) → ¬ 𝑦 ≼ ω )
128		pm2.53	⊢ ( ( 𝑦 ≼ ω ∨ ( 𝐴 ∖ 𝑦 ) ≼ ω ) → ( ¬ 𝑦 ≼ ω → ( 𝐴 ∖ 𝑦 ) ≼ ω ) )
129	126 127 128	sylc	⊢ ( ( 𝑦 ∈ 𝑆 ∧ ¬ 𝑦 ≼ ω ) → ( 𝐴 ∖ 𝑦 ) ≼ ω )
130	121 122 129	syl2anc	⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω ) → ( 𝐴 ∖ 𝑦 ) ≼ ω )
131		ssct	⊢ ( ( ( 𝐴 ∖ ∪ 𝑥 ) ⊆ ( 𝐴 ∖ 𝑦 ) ∧ ( 𝐴 ∖ 𝑦 ) ≼ ω ) → ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω )
132	120 130 131	syl2anc	⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω ) → ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω )
133	132	3exp	⊢ ( 𝑥 ∈ 𝒫 𝑆 → ( 𝑦 ∈ 𝑥 → ( ¬ 𝑦 ≼ ω → ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) ) )
134	133	adantr	⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω ) → ( 𝑦 ∈ 𝑥 → ( ¬ 𝑦 ≼ ω → ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) ) )
135	116 117 134	rexlimd	⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω ) → ( ∃ 𝑦 ∈ 𝑥 ¬ 𝑦 ≼ ω → ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) )
136	112 135	mpd	⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω ) → ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω )
137		olc	⊢ ( ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω → ( ∪ 𝑥 ≼ ω ∨ ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) )
138	136 137	syl	⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω ) → ( ∪ 𝑥 ≼ ω ∨ ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) )
139	138	adantlr	⊢ ( ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω ) ∧ ¬ ∀ 𝑦 ∈ 𝑥 𝑦 ≼ ω ) → ( ∪ 𝑥 ≼ ω ∨ ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) )
140	108 139	pm2.61dan	⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω ) → ( ∪ 𝑥 ≼ ω ∨ ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) )
141	103 140	jca	⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω ) → ( ∪ 𝑥 ∈ 𝒫 𝐴 ∧ ( ∪ 𝑥 ≼ ω ∨ ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) ) )
142		breq1	⊢ ( 𝑦 = ∪ 𝑥 → ( 𝑦 ≼ ω ↔ ∪ 𝑥 ≼ ω ) )
143		difeq2	⊢ ( 𝑦 = ∪ 𝑥 → ( 𝐴 ∖ 𝑦 ) = ( 𝐴 ∖ ∪ 𝑥 ) )
144	143	breq1d	⊢ ( 𝑦 = ∪ 𝑥 → ( ( 𝐴 ∖ 𝑦 ) ≼ ω ↔ ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) )
145	142 144	orbi12d	⊢ ( 𝑦 = ∪ 𝑥 → ( ( 𝑦 ≼ ω ∨ ( 𝐴 ∖ 𝑦 ) ≼ ω ) ↔ ( ∪ 𝑥 ≼ ω ∨ ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) ) )
146	145 72	elrab2	⊢ ( ∪ 𝑥 ∈ 𝑆 ↔ ( ∪ 𝑥 ∈ 𝒫 𝐴 ∧ ( ∪ 𝑥 ≼ ω ∨ ( 𝐴 ∖ ∪ 𝑥 ) ≼ ω ) ) )
147	141 146	sylibr	⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω ) → ∪ 𝑥 ∈ 𝑆 )
148	147	3adant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω ) → ∪ 𝑥 ∈ 𝑆 )
149	6 20 45 88 148	issald	⊢ ( 𝜑 → 𝑆 ∈ SAlg )