Theorem prsiga 34128

Description: The smallest possible sigma-algebra containing 𝑂. (Contributed by Thierry Arnoux, 13-Sep-2016.)

Assertion

Ref	Expression
prsiga	⊢ (𝑂 ∈ 𝑉 → {∅, 𝑂} ∈ (sigAlgebra‘𝑂))

Proof of Theorem prsiga

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		0elpw 5314	. . 3 ⊢ ∅ ∈ 𝒫 𝑂
2		pwidg 4586	. . 3 ⊢ (𝑂 ∈ 𝑉 → 𝑂 ∈ 𝒫 𝑂)
3		prssi 4788	. . 3 ⊢ ((∅ ∈ 𝒫 𝑂 ∧ 𝑂 ∈ 𝒫 𝑂) → {∅, 𝑂} ⊆ 𝒫 𝑂)
4	1, 2, 3	sylancr 587	. 2 ⊢ (𝑂 ∈ 𝑉 → {∅, 𝑂} ⊆ 𝒫 𝑂)
5		prid2g 4728	. . 3 ⊢ (𝑂 ∈ 𝑉 → 𝑂 ∈ {∅, 𝑂})
6		dif0 4344	. . . . 5 ⊢ (𝑂 ∖ ∅) = 𝑂
7	6, 5	eqeltrid 2833	. . . 4 ⊢ (𝑂 ∈ 𝑉 → (𝑂 ∖ ∅) ∈ {∅, 𝑂})
8		difid 4342	. . . . 5 ⊢ (𝑂 ∖ 𝑂) = ∅
9		0ex 5265	. . . . . . 7 ⊢ ∅ ∈ V
10	9	prid1 4729	. . . . . 6 ⊢ ∅ ∈ {∅, 𝑂}
11	10	a1i 11	. . . . 5 ⊢ (𝑂 ∈ 𝑉 → ∅ ∈ {∅, 𝑂})
12	8, 11	eqeltrid 2833	. . . 4 ⊢ (𝑂 ∈ 𝑉 → (𝑂 ∖ 𝑂) ∈ {∅, 𝑂})
13		difeq2 4086	. . . . . . 7 ⊢ (𝑥 = ∅ → (𝑂 ∖ 𝑥) = (𝑂 ∖ ∅))
14	13	eleq1d 2814	. . . . . 6 ⊢ (𝑥 = ∅ → ((𝑂 ∖ 𝑥) ∈ {∅, 𝑂} ↔ (𝑂 ∖ ∅) ∈ {∅, 𝑂}))
15		difeq2 4086	. . . . . . 7 ⊢ (𝑥 = 𝑂 → (𝑂 ∖ 𝑥) = (𝑂 ∖ 𝑂))
16	15	eleq1d 2814	. . . . . 6 ⊢ (𝑥 = 𝑂 → ((𝑂 ∖ 𝑥) ∈ {∅, 𝑂} ↔ (𝑂 ∖ 𝑂) ∈ {∅, 𝑂}))
17	14, 16	ralprg 4663	. . . . 5 ⊢ ((∅ ∈ V ∧ 𝑂 ∈ 𝑉) → (∀𝑥 ∈ {∅, 𝑂} (𝑂 ∖ 𝑥) ∈ {∅, 𝑂} ↔ ((𝑂 ∖ ∅) ∈ {∅, 𝑂} ∧ (𝑂 ∖ 𝑂) ∈ {∅, 𝑂})))
18	9, 17	mpan 690	. . . 4 ⊢ (𝑂 ∈ 𝑉 → (∀𝑥 ∈ {∅, 𝑂} (𝑂 ∖ 𝑥) ∈ {∅, 𝑂} ↔ ((𝑂 ∖ ∅) ∈ {∅, 𝑂} ∧ (𝑂 ∖ 𝑂) ∈ {∅, 𝑂})))
19	7, 12, 18	mpbir2and 713	. . 3 ⊢ (𝑂 ∈ 𝑉 → ∀𝑥 ∈ {∅, 𝑂} (𝑂 ∖ 𝑥) ∈ {∅, 𝑂})
20		uni0 4902	. . . . . . . . 9 ⊢ ∪ ∅ = ∅
21	20, 10	eqeltri 2825	. . . . . . . 8 ⊢ ∪ ∅ ∈ {∅, 𝑂}
22	9	unisn 4893	. . . . . . . . 9 ⊢ ∪ {∅} = ∅
23	22, 10	eqeltri 2825	. . . . . . . 8 ⊢ ∪ {∅} ∈ {∅, 𝑂}
24	21, 23	pm3.2i 470	. . . . . . 7 ⊢ (∪ ∅ ∈ {∅, 𝑂} ∧ ∪ {∅} ∈ {∅, 𝑂})
25		snex 5394	. . . . . . . . 9 ⊢ {∅} ∈ V
26	9, 25	pm3.2i 470	. . . . . . . 8 ⊢ (∅ ∈ V ∧ {∅} ∈ V)
27		unieq 4885	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → ∪ 𝑥 = ∪ ∅)
28	27	eleq1d 2814	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (∪ 𝑥 ∈ {∅, 𝑂} ↔ ∪ ∅ ∈ {∅, 𝑂}))
29		unieq 4885	. . . . . . . . . 10 ⊢ (𝑥 = {∅} → ∪ 𝑥 = ∪ {∅})
30	29	eleq1d 2814	. . . . . . . . 9 ⊢ (𝑥 = {∅} → (∪ 𝑥 ∈ {∅, 𝑂} ↔ ∪ {∅} ∈ {∅, 𝑂}))
31	28, 30	ralprg 4663	. . . . . . . 8 ⊢ ((∅ ∈ V ∧ {∅} ∈ V) → (∀𝑥 ∈ {∅, {∅}}∪ 𝑥 ∈ {∅, 𝑂} ↔ (∪ ∅ ∈ {∅, 𝑂} ∧ ∪ {∅} ∈ {∅, 𝑂})))
32	26, 31	mp1i 13	. . . . . . 7 ⊢ (𝑂 ∈ 𝑉 → (∀𝑥 ∈ {∅, {∅}}∪ 𝑥 ∈ {∅, 𝑂} ↔ (∪ ∅ ∈ {∅, 𝑂} ∧ ∪ {∅} ∈ {∅, 𝑂})))
33	24, 32	mpbiri 258	. . . . . 6 ⊢ (𝑂 ∈ 𝑉 → ∀𝑥 ∈ {∅, {∅}}∪ 𝑥 ∈ {∅, 𝑂})
34		unisng 4892	. . . . . . . 8 ⊢ (𝑂 ∈ 𝑉 → ∪ {𝑂} = 𝑂)
35	34, 5	eqeltrd 2829	. . . . . . 7 ⊢ (𝑂 ∈ 𝑉 → ∪ {𝑂} ∈ {∅, 𝑂})
36		uniprg 4890	. . . . . . . . . 10 ⊢ ((∅ ∈ V ∧ 𝑂 ∈ 𝑉) → ∪ {∅, 𝑂} = (∅ ∪ 𝑂))
37	9, 36	mpan 690	. . . . . . . . 9 ⊢ (𝑂 ∈ 𝑉 → ∪ {∅, 𝑂} = (∅ ∪ 𝑂))
38		uncom 4124	. . . . . . . . . 10 ⊢ (∅ ∪ 𝑂) = (𝑂 ∪ ∅)
39		un0 4360	. . . . . . . . . 10 ⊢ (𝑂 ∪ ∅) = 𝑂
40	38, 39	eqtri 2753	. . . . . . . . 9 ⊢ (∅ ∪ 𝑂) = 𝑂
41	37, 40	eqtrdi 2781	. . . . . . . 8 ⊢ (𝑂 ∈ 𝑉 → ∪ {∅, 𝑂} = 𝑂)
42	41, 5	eqeltrd 2829	. . . . . . 7 ⊢ (𝑂 ∈ 𝑉 → ∪ {∅, 𝑂} ∈ {∅, 𝑂})
43		snex 5394	. . . . . . . . 9 ⊢ {𝑂} ∈ V
44		prex 5395	. . . . . . . . 9 ⊢ {∅, 𝑂} ∈ V
45	43, 44	pm3.2i 470	. . . . . . . 8 ⊢ ({𝑂} ∈ V ∧ {∅, 𝑂} ∈ V)
46		unieq 4885	. . . . . . . . . 10 ⊢ (𝑥 = {𝑂} → ∪ 𝑥 = ∪ {𝑂})
47	46	eleq1d 2814	. . . . . . . . 9 ⊢ (𝑥 = {𝑂} → (∪ 𝑥 ∈ {∅, 𝑂} ↔ ∪ {𝑂} ∈ {∅, 𝑂}))
48		unieq 4885	. . . . . . . . . 10 ⊢ (𝑥 = {∅, 𝑂} → ∪ 𝑥 = ∪ {∅, 𝑂})
49	48	eleq1d 2814	. . . . . . . . 9 ⊢ (𝑥 = {∅, 𝑂} → (∪ 𝑥 ∈ {∅, 𝑂} ↔ ∪ {∅, 𝑂} ∈ {∅, 𝑂}))
50	47, 49	ralprg 4663	. . . . . . . 8 ⊢ (({𝑂} ∈ V ∧ {∅, 𝑂} ∈ V) → (∀𝑥 ∈ {{𝑂}, {∅, 𝑂}}∪ 𝑥 ∈ {∅, 𝑂} ↔ (∪ {𝑂} ∈ {∅, 𝑂} ∧ ∪ {∅, 𝑂} ∈ {∅, 𝑂})))
51	45, 50	mp1i 13	. . . . . . 7 ⊢ (𝑂 ∈ 𝑉 → (∀𝑥 ∈ {{𝑂}, {∅, 𝑂}}∪ 𝑥 ∈ {∅, 𝑂} ↔ (∪ {𝑂} ∈ {∅, 𝑂} ∧ ∪ {∅, 𝑂} ∈ {∅, 𝑂})))
52	35, 42, 51	mpbir2and 713	. . . . . 6 ⊢ (𝑂 ∈ 𝑉 → ∀𝑥 ∈ {{𝑂}, {∅, 𝑂}}∪ 𝑥 ∈ {∅, 𝑂})
53		ralun 4164	. . . . . 6 ⊢ ((∀𝑥 ∈ {∅, {∅}}∪ 𝑥 ∈ {∅, 𝑂} ∧ ∀𝑥 ∈ {{𝑂}, {∅, 𝑂}}∪ 𝑥 ∈ {∅, 𝑂}) → ∀𝑥 ∈ ({∅, {∅}} ∪ {{𝑂}, {∅, 𝑂}})∪ 𝑥 ∈ {∅, 𝑂})
54	33, 52, 53	syl2anc 584	. . . . 5 ⊢ (𝑂 ∈ 𝑉 → ∀𝑥 ∈ ({∅, {∅}} ∪ {{𝑂}, {∅, 𝑂}})∪ 𝑥 ∈ {∅, 𝑂})
55		pwpr 4868	. . . . . 6 ⊢ 𝒫 {∅, 𝑂} = ({∅, {∅}} ∪ {{𝑂}, {∅, 𝑂}})
56	55	raleqi 3299	. . . . 5 ⊢ (∀𝑥 ∈ 𝒫 {∅, 𝑂}∪ 𝑥 ∈ {∅, 𝑂} ↔ ∀𝑥 ∈ ({∅, {∅}} ∪ {{𝑂}, {∅, 𝑂}})∪ 𝑥 ∈ {∅, 𝑂})
57	54, 56	sylibr 234	. . . 4 ⊢ (𝑂 ∈ 𝑉 → ∀𝑥 ∈ 𝒫 {∅, 𝑂}∪ 𝑥 ∈ {∅, 𝑂})
58		ax-1 6	. . . . 5 ⊢ (∪ 𝑥 ∈ {∅, 𝑂} → (𝑥 ≼ ω → ∪ 𝑥 ∈ {∅, 𝑂}))
59	58	ralimi 3067	. . . 4 ⊢ (∀𝑥 ∈ 𝒫 {∅, 𝑂}∪ 𝑥 ∈ {∅, 𝑂} → ∀𝑥 ∈ 𝒫 {∅, 𝑂} (𝑥 ≼ ω → ∪ 𝑥 ∈ {∅, 𝑂}))
60	57, 59	syl 17	. . 3 ⊢ (𝑂 ∈ 𝑉 → ∀𝑥 ∈ 𝒫 {∅, 𝑂} (𝑥 ≼ ω → ∪ 𝑥 ∈ {∅, 𝑂}))
61	5, 19, 60	3jca 1128	. 2 ⊢ (𝑂 ∈ 𝑉 → (𝑂 ∈ {∅, 𝑂} ∧ ∀𝑥 ∈ {∅, 𝑂} (𝑂 ∖ 𝑥) ∈ {∅, 𝑂} ∧ ∀𝑥 ∈ 𝒫 {∅, 𝑂} (𝑥 ≼ ω → ∪ 𝑥 ∈ {∅, 𝑂})))
62		issiga 34109	. . 3 ⊢ ({∅, 𝑂} ∈ V → ({∅, 𝑂} ∈ (sigAlgebra‘𝑂) ↔ ({∅, 𝑂} ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ {∅, 𝑂} ∧ ∀𝑥 ∈ {∅, 𝑂} (𝑂 ∖ 𝑥) ∈ {∅, 𝑂} ∧ ∀𝑥 ∈ 𝒫 {∅, 𝑂} (𝑥 ≼ ω → ∪ 𝑥 ∈ {∅, 𝑂})))))
63	44, 62	ax-mp 5	. 2 ⊢ ({∅, 𝑂} ∈ (sigAlgebra‘𝑂) ↔ ({∅, 𝑂} ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ {∅, 𝑂} ∧ ∀𝑥 ∈ {∅, 𝑂} (𝑂 ∖ 𝑥) ∈ {∅, 𝑂} ∧ ∀𝑥 ∈ 𝒫 {∅, 𝑂} (𝑥 ≼ ω → ∪ 𝑥 ∈ {∅, 𝑂}))))
64	4, 61, 63	sylanbrc 583	1 ⊢ (𝑂 ∈ 𝑉 → {∅, 𝑂} ∈ (sigAlgebra‘𝑂))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∀wral 3045  Vcvv 3450   ∖ cdif 3914   ∪ cun 3915   ⊆ wss 3917  ∅c0 4299  𝒫 cpw 4566  {csn 4592  {cpr 4594  ∪ cuni 4874   class class class wbr 5110  ‘cfv 6514  ωcom 7845   ≼ cdom 8919  sigAlgebracsiga 34105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-iota 6467  df-fun 6516  df-fv 6522  df-siga 34106

This theorem is referenced by: (None)