| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ssrab2 4079 | . . 3
⊢ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ⊆ 𝒫 𝑂 | 
| 2 |  | dynkin.o | . . . 4
⊢ (𝜑 → 𝑂 ∈ 𝑉) | 
| 3 |  | pwexg 5377 | . . . 4
⊢ (𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ V) | 
| 4 |  | rabexg 5336 | . . . 4
⊢
(𝒫 𝑂 ∈
V → {𝑏 ∈
𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ∈ V) | 
| 5 |  | elpwg 4602 | . . . 4
⊢ ({𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ∈ V → ({𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ∈ 𝒫 𝒫 𝑂 ↔ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ⊆ 𝒫 𝑂)) | 
| 6 | 2, 3, 4, 5 | 4syl 19 | . . 3
⊢ (𝜑 → ({𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ∈ 𝒫 𝒫 𝑂 ↔ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ⊆ 𝒫 𝑂)) | 
| 7 | 1, 6 | mpbiri 258 | . 2
⊢ (𝜑 → {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ∈ 𝒫 𝒫 𝑂) | 
| 8 |  | ineq2 4213 | . . . . 5
⊢ (𝑏 = ∅ → (𝐴 ∩ 𝑏) = (𝐴 ∩ ∅)) | 
| 9 | 8 | eleq1d 2825 | . . . 4
⊢ (𝑏 = ∅ → ((𝐴 ∩ 𝑏) ∈ 𝐸 ↔ (𝐴 ∩ ∅) ∈ 𝐸)) | 
| 10 |  | 0elpw 5355 | . . . . 5
⊢ ∅
∈ 𝒫 𝑂 | 
| 11 | 10 | a1i 11 | . . . 4
⊢ (𝜑 → ∅ ∈ 𝒫
𝑂) | 
| 12 |  | dynkin.l | . . . . . . . . . . . 12
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} | 
| 13 | 12 | isldsys 34158 | . . . . . . . . . . 11
⊢ (𝑡 ∈ 𝐿 ↔ (𝑡 ∈ 𝒫 𝒫 𝑂 ∧ (∅ ∈ 𝑡 ∧ ∀𝑥 ∈ 𝑡 (𝑂 ∖ 𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑡)))) | 
| 14 | 13 | simprbi 496 | . . . . . . . . . 10
⊢ (𝑡 ∈ 𝐿 → (∅ ∈ 𝑡 ∧ ∀𝑥 ∈ 𝑡 (𝑂 ∖ 𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑡))) | 
| 15 | 14 | simp1d 1142 | . . . . . . . . 9
⊢ (𝑡 ∈ 𝐿 → ∅ ∈ 𝑡) | 
| 16 | 15 | ad2antlr 727 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → ∅ ∈ 𝑡) | 
| 17 | 16 | ex 412 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → (𝑇 ⊆ 𝑡 → ∅ ∈ 𝑡)) | 
| 18 | 17 | ralrimiva 3145 | . . . . . 6
⊢ (𝜑 → ∀𝑡 ∈ 𝐿 (𝑇 ⊆ 𝑡 → ∅ ∈ 𝑡)) | 
| 19 |  | 0ex 5306 | . . . . . . 7
⊢ ∅
∈ V | 
| 20 | 19 | elintrab 4959 | . . . . . 6
⊢ (∅
∈ ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡} ↔ ∀𝑡 ∈ 𝐿 (𝑇 ⊆ 𝑡 → ∅ ∈ 𝑡)) | 
| 21 | 18, 20 | sylibr 234 | . . . . 5
⊢ (𝜑 → ∅ ∈ ∩ {𝑡
∈ 𝐿 ∣ 𝑇 ⊆ 𝑡}) | 
| 22 |  | in0 4394 | . . . . 5
⊢ (𝐴 ∩ ∅) =
∅ | 
| 23 |  | ldgenpisys.e | . . . . 5
⊢ 𝐸 = ∩
{𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡} | 
| 24 | 21, 22, 23 | 3eltr4g 2857 | . . . 4
⊢ (𝜑 → (𝐴 ∩ ∅) ∈ 𝐸) | 
| 25 | 9, 11, 24 | elrabd 3693 | . . 3
⊢ (𝜑 → ∅ ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) | 
| 26 |  | ineq2 4213 | . . . . . . . 8
⊢ (𝑏 = 𝑥 → (𝐴 ∩ 𝑏) = (𝐴 ∩ 𝑥)) | 
| 27 | 26 | eleq1d 2825 | . . . . . . 7
⊢ (𝑏 = 𝑥 → ((𝐴 ∩ 𝑏) ∈ 𝐸 ↔ (𝐴 ∩ 𝑥) ∈ 𝐸)) | 
| 28 | 27 | elrab 3691 | . . . . . 6
⊢ (𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ↔ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) | 
| 29 |  | pwidg 4619 | . . . . . . . . . 10
⊢ (𝑂 ∈ 𝑉 → 𝑂 ∈ 𝒫 𝑂) | 
| 30 | 2, 29 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑂 ∈ 𝒫 𝑂) | 
| 31 | 30 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) → 𝑂 ∈ 𝒫 𝑂) | 
| 32 | 31 | elpwdifcl 32546 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) → (𝑂 ∖ 𝑥) ∈ 𝒫 𝑂) | 
| 33 | 12 | pwldsys 34159 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ 𝐿) | 
| 34 | 2, 33 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝒫 𝑂 ∈ 𝐿) | 
| 35 |  | ldgenpisys.1 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑇 ∈ 𝑃) | 
| 36 |  | dynkin.p | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} | 
| 37 | 36 | ispisys 34154 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑇 ∈ 𝑃 ↔ (𝑇 ∈ 𝒫 𝒫 𝑂 ∧ (fi‘𝑇) ⊆ 𝑇)) | 
| 38 | 35, 37 | sylib 218 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑇 ∈ 𝒫 𝒫 𝑂 ∧ (fi‘𝑇) ⊆ 𝑇)) | 
| 39 | 38 | simpld 494 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑇 ∈ 𝒫 𝒫 𝑂) | 
| 40 | 39 | elpwid 4608 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑇 ⊆ 𝒫 𝑂) | 
| 41 |  | sseq2 4009 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝒫 𝑂 → (𝑇 ⊆ 𝑡 ↔ 𝑇 ⊆ 𝒫 𝑂)) | 
| 42 | 41 | intminss 4973 | . . . . . . . . . . . . . . . . . 18
⊢
((𝒫 𝑂 ∈
𝐿 ∧ 𝑇 ⊆ 𝒫 𝑂) → ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡} ⊆ 𝒫 𝑂) | 
| 43 | 34, 40, 42 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∩ {𝑡
∈ 𝐿 ∣ 𝑇 ⊆ 𝑡} ⊆ 𝒫 𝑂) | 
| 44 | 23, 43 | eqsstrid 4021 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐸 ⊆ 𝒫 𝑂) | 
| 45 |  | ldgenpisyslem1.1 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ 𝐸) | 
| 46 | 44, 45 | sseldd 3983 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ 𝒫 𝑂) | 
| 47 | 46 | elpwid 4608 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ⊆ 𝑂) | 
| 48 | 47 | ad3antrrr 730 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → 𝐴 ⊆ 𝑂) | 
| 49 |  | difin 4271 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ∖ (𝐴 ∩ 𝑥)) = (𝐴 ∖ 𝑥) | 
| 50 |  | difin2 4300 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ⊆ 𝑂 → (𝐴 ∖ 𝑥) = ((𝑂 ∖ 𝑥) ∩ 𝐴)) | 
| 51 | 49, 50 | eqtrid 2788 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ⊆ 𝑂 → (𝐴 ∖ (𝐴 ∩ 𝑥)) = ((𝑂 ∖ 𝑥) ∩ 𝐴)) | 
| 52 |  | incom 4208 | . . . . . . . . . . . . . . 15
⊢ ((𝑂 ∖ 𝑥) ∩ 𝐴) = (𝐴 ∩ (𝑂 ∖ 𝑥)) | 
| 53 | 51, 52 | eqtrdi 2792 | . . . . . . . . . . . . . 14
⊢ (𝐴 ⊆ 𝑂 → (𝐴 ∖ (𝐴 ∩ 𝑥)) = (𝐴 ∩ (𝑂 ∖ 𝑥))) | 
| 54 |  | difuncomp 32567 | . . . . . . . . . . . . . 14
⊢ (𝐴 ⊆ 𝑂 → (𝐴 ∖ (𝐴 ∩ 𝑥)) = (𝑂 ∖ ((𝑂 ∖ 𝐴) ∪ (𝐴 ∩ 𝑥)))) | 
| 55 | 53, 54 | eqtr3d 2778 | . . . . . . . . . . . . 13
⊢ (𝐴 ⊆ 𝑂 → (𝐴 ∩ (𝑂 ∖ 𝑥)) = (𝑂 ∖ ((𝑂 ∖ 𝐴) ∪ (𝐴 ∩ 𝑥)))) | 
| 56 | 48, 55 | syl 17 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → (𝐴 ∩ (𝑂 ∖ 𝑥)) = (𝑂 ∖ ((𝑂 ∖ 𝐴) ∪ (𝐴 ∩ 𝑥)))) | 
| 57 |  | difeq2 4119 | . . . . . . . . . . . . . 14
⊢ (𝑦 = ((𝑂 ∖ 𝐴) ∪ (𝐴 ∩ 𝑥)) → (𝑂 ∖ 𝑦) = (𝑂 ∖ ((𝑂 ∖ 𝐴) ∪ (𝐴 ∩ 𝑥)))) | 
| 58 | 57 | eleq1d 2825 | . . . . . . . . . . . . 13
⊢ (𝑦 = ((𝑂 ∖ 𝐴) ∪ (𝐴 ∩ 𝑥)) → ((𝑂 ∖ 𝑦) ∈ 𝑡 ↔ (𝑂 ∖ ((𝑂 ∖ 𝐴) ∪ (𝐴 ∩ 𝑥))) ∈ 𝑡)) | 
| 59 | 14 | simp2d 1143 | . . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ 𝐿 → ∀𝑥 ∈ 𝑡 (𝑂 ∖ 𝑥) ∈ 𝑡) | 
| 60 | 59 | ad2antlr 727 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → ∀𝑥 ∈ 𝑡 (𝑂 ∖ 𝑥) ∈ 𝑡) | 
| 61 |  | difeq2 4119 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝑂 ∖ 𝑥) = (𝑂 ∖ 𝑦)) | 
| 62 | 61 | eleq1d 2825 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → ((𝑂 ∖ 𝑥) ∈ 𝑡 ↔ (𝑂 ∖ 𝑦) ∈ 𝑡)) | 
| 63 | 62 | cbvralvw 3236 | . . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
𝑡 (𝑂 ∖ 𝑥) ∈ 𝑡 ↔ ∀𝑦 ∈ 𝑡 (𝑂 ∖ 𝑦) ∈ 𝑡) | 
| 64 | 60, 63 | sylib 218 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → ∀𝑦 ∈ 𝑡 (𝑂 ∖ 𝑦) ∈ 𝑡) | 
| 65 |  | simplr 768 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → 𝑡 ∈ 𝐿) | 
| 66 | 45, 23 | eleqtrdi 2850 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴 ∈ ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡}) | 
| 67 |  | elintrabg 4960 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ 𝐸 → (𝐴 ∈ ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡} ↔ ∀𝑡 ∈ 𝐿 (𝑇 ⊆ 𝑡 → 𝐴 ∈ 𝑡))) | 
| 68 | 45, 67 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐴 ∈ ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡} ↔ ∀𝑡 ∈ 𝐿 (𝑇 ⊆ 𝑡 → 𝐴 ∈ 𝑡))) | 
| 69 | 66, 68 | mpbid 232 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑡 ∈ 𝐿 (𝑇 ⊆ 𝑡 → 𝐴 ∈ 𝑡)) | 
| 70 | 69 | r19.21bi 3250 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → (𝑇 ⊆ 𝑡 → 𝐴 ∈ 𝑡)) | 
| 71 | 70 | imp 406 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → 𝐴 ∈ 𝑡) | 
| 72 | 71 | adantllr 719 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → 𝐴 ∈ 𝑡) | 
| 73 |  | difeq2 4119 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝐴 → (𝑂 ∖ 𝑥) = (𝑂 ∖ 𝐴)) | 
| 74 | 73 | eleq1d 2825 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝐴 → ((𝑂 ∖ 𝑥) ∈ 𝑡 ↔ (𝑂 ∖ 𝐴) ∈ 𝑡)) | 
| 75 | 59 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ 𝐿 ∧ 𝐴 ∈ 𝑡) → ∀𝑥 ∈ 𝑡 (𝑂 ∖ 𝑥) ∈ 𝑡) | 
| 76 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ 𝐿 ∧ 𝐴 ∈ 𝑡) → 𝐴 ∈ 𝑡) | 
| 77 | 74, 75, 76 | rspcdva 3622 | . . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ 𝐿 ∧ 𝐴 ∈ 𝑡) → (𝑂 ∖ 𝐴) ∈ 𝑡) | 
| 78 | 65, 72, 77 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → (𝑂 ∖ 𝐴) ∈ 𝑡) | 
| 79 |  | simpllr 775 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) | 
| 80 | 79 | simprd 495 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → (𝐴 ∩ 𝑥) ∈ 𝐸) | 
| 81 | 80, 23 | eleqtrdi 2850 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → (𝐴 ∩ 𝑥) ∈ ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡}) | 
| 82 |  | vex 3483 | . . . . . . . . . . . . . . . . . 18
⊢ 𝑥 ∈ V | 
| 83 | 82 | inex2 5317 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∩ 𝑥) ∈ V | 
| 84 |  | elintrabg 4960 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∩ 𝑥) ∈ V → ((𝐴 ∩ 𝑥) ∈ ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡} ↔ ∀𝑡 ∈ 𝐿 (𝑇 ⊆ 𝑡 → (𝐴 ∩ 𝑥) ∈ 𝑡))) | 
| 85 | 83, 84 | mp1i 13 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → ((𝐴 ∩ 𝑥) ∈ ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡} ↔ ∀𝑡 ∈ 𝐿 (𝑇 ⊆ 𝑡 → (𝐴 ∩ 𝑥) ∈ 𝑡))) | 
| 86 | 81, 85 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → ∀𝑡 ∈ 𝐿 (𝑇 ⊆ 𝑡 → (𝐴 ∩ 𝑥) ∈ 𝑡)) | 
| 87 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → 𝑇 ⊆ 𝑡) | 
| 88 |  | rspa 3247 | . . . . . . . . . . . . . . . 16
⊢
((∀𝑡 ∈
𝐿 (𝑇 ⊆ 𝑡 → (𝐴 ∩ 𝑥) ∈ 𝑡) ∧ 𝑡 ∈ 𝐿) → (𝑇 ⊆ 𝑡 → (𝐴 ∩ 𝑥) ∈ 𝑡)) | 
| 89 | 88 | imp 406 | . . . . . . . . . . . . . . 15
⊢
(((∀𝑡 ∈
𝐿 (𝑇 ⊆ 𝑡 → (𝐴 ∩ 𝑥) ∈ 𝑡) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → (𝐴 ∩ 𝑥) ∈ 𝑡) | 
| 90 | 86, 65, 87, 89 | syl21anc 837 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → (𝐴 ∩ 𝑥) ∈ 𝑡) | 
| 91 |  | incom 4208 | . . . . . . . . . . . . . . . 16
⊢ ((𝑂 ∖ 𝐴) ∩ (𝐴 ∩ 𝑥)) = ((𝐴 ∩ 𝑥) ∩ (𝑂 ∖ 𝐴)) | 
| 92 |  | inss1 4236 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∩ 𝑥) ⊆ 𝐴 | 
| 93 |  | disjdif 4471 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∩ (𝑂 ∖ 𝐴)) = ∅ | 
| 94 |  | ssdisj 4459 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∩ 𝑥) ⊆ 𝐴 ∧ (𝐴 ∩ (𝑂 ∖ 𝐴)) = ∅) → ((𝐴 ∩ 𝑥) ∩ (𝑂 ∖ 𝐴)) = ∅) | 
| 95 | 92, 93, 94 | mp2an 692 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∩ 𝑥) ∩ (𝑂 ∖ 𝐴)) = ∅ | 
| 96 | 91, 95 | eqtri 2764 | . . . . . . . . . . . . . . 15
⊢ ((𝑂 ∖ 𝐴) ∩ (𝐴 ∩ 𝑥)) = ∅ | 
| 97 | 96 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → ((𝑂 ∖ 𝐴) ∩ (𝐴 ∩ 𝑥)) = ∅) | 
| 98 | 12, 65, 78, 90, 97 | unelldsys 34160 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → ((𝑂 ∖ 𝐴) ∪ (𝐴 ∩ 𝑥)) ∈ 𝑡) | 
| 99 | 58, 64, 98 | rspcdva 3622 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → (𝑂 ∖ ((𝑂 ∖ 𝐴) ∪ (𝐴 ∩ 𝑥))) ∈ 𝑡) | 
| 100 | 56, 99 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → (𝐴 ∩ (𝑂 ∖ 𝑥)) ∈ 𝑡) | 
| 101 | 100 | ex 412 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) ∧ 𝑡 ∈ 𝐿) → (𝑇 ⊆ 𝑡 → (𝐴 ∩ (𝑂 ∖ 𝑥)) ∈ 𝑡)) | 
| 102 | 101 | ralrimiva 3145 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) → ∀𝑡 ∈ 𝐿 (𝑇 ⊆ 𝑡 → (𝐴 ∩ (𝑂 ∖ 𝑥)) ∈ 𝑡)) | 
| 103 |  | inex1g 5318 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝐸 → (𝐴 ∩ (𝑂 ∖ 𝑥)) ∈ V) | 
| 104 | 45, 103 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐴 ∩ (𝑂 ∖ 𝑥)) ∈ V) | 
| 105 | 104 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) → (𝐴 ∩ (𝑂 ∖ 𝑥)) ∈ V) | 
| 106 |  | elintrabg 4960 | . . . . . . . . . 10
⊢ ((𝐴 ∩ (𝑂 ∖ 𝑥)) ∈ V → ((𝐴 ∩ (𝑂 ∖ 𝑥)) ∈ ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡} ↔ ∀𝑡 ∈ 𝐿 (𝑇 ⊆ 𝑡 → (𝐴 ∩ (𝑂 ∖ 𝑥)) ∈ 𝑡))) | 
| 107 | 105, 106 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) → ((𝐴 ∩ (𝑂 ∖ 𝑥)) ∈ ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡} ↔ ∀𝑡 ∈ 𝐿 (𝑇 ⊆ 𝑡 → (𝐴 ∩ (𝑂 ∖ 𝑥)) ∈ 𝑡))) | 
| 108 | 102, 107 | mpbird 257 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) → (𝐴 ∩ (𝑂 ∖ 𝑥)) ∈ ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡}) | 
| 109 | 108, 23 | eleqtrrdi 2851 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) → (𝐴 ∩ (𝑂 ∖ 𝑥)) ∈ 𝐸) | 
| 110 | 32, 109 | jca 511 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑥) ∈ 𝐸)) → ((𝑂 ∖ 𝑥) ∈ 𝒫 𝑂 ∧ (𝐴 ∩ (𝑂 ∖ 𝑥)) ∈ 𝐸)) | 
| 111 | 28, 110 | sylan2b 594 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) → ((𝑂 ∖ 𝑥) ∈ 𝒫 𝑂 ∧ (𝐴 ∩ (𝑂 ∖ 𝑥)) ∈ 𝐸)) | 
| 112 |  | ineq2 4213 | . . . . . . 7
⊢ (𝑏 = (𝑂 ∖ 𝑥) → (𝐴 ∩ 𝑏) = (𝐴 ∩ (𝑂 ∖ 𝑥))) | 
| 113 | 112 | eleq1d 2825 | . . . . . 6
⊢ (𝑏 = (𝑂 ∖ 𝑥) → ((𝐴 ∩ 𝑏) ∈ 𝐸 ↔ (𝐴 ∩ (𝑂 ∖ 𝑥)) ∈ 𝐸)) | 
| 114 | 113 | elrab 3691 | . . . . 5
⊢ ((𝑂 ∖ 𝑥) ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ↔ ((𝑂 ∖ 𝑥) ∈ 𝒫 𝑂 ∧ (𝐴 ∩ (𝑂 ∖ 𝑥)) ∈ 𝐸)) | 
| 115 | 111, 114 | sylibr 234 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) → (𝑂 ∖ 𝑥) ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) | 
| 116 | 115 | ralrimiva 3145 | . . 3
⊢ (𝜑 → ∀𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} (𝑂 ∖ 𝑥) ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) | 
| 117 |  | ineq2 4213 | . . . . . . 7
⊢ (𝑏 = ∪
𝑥 → (𝐴 ∩ 𝑏) = (𝐴 ∩ ∪ 𝑥)) | 
| 118 | 117 | eleq1d 2825 | . . . . . 6
⊢ (𝑏 = ∪
𝑥 → ((𝐴 ∩ 𝑏) ∈ 𝐸 ↔ (𝐴 ∩ ∪ 𝑥) ∈ 𝐸)) | 
| 119 | 1 | sspwi 4611 | . . . . . . . 8
⊢ 𝒫
{𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ⊆ 𝒫 𝒫 𝑂 | 
| 120 |  | simplr 768 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) | 
| 121 | 119, 120 | sselid 3980 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → 𝑥 ∈ 𝒫 𝒫 𝑂) | 
| 122 | 121 | elpwunicl 32568 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → ∪ 𝑥 ∈ 𝒫 𝑂) | 
| 123 |  | uniin2 32566 | . . . . . . . . . . . 12
⊢ ∪ 𝑦 ∈ 𝑥 (𝐴 ∩ 𝑦) = (𝐴 ∩ ∪ 𝑥) | 
| 124 |  | vex 3483 | . . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V | 
| 125 | 124 | inex2 5317 | . . . . . . . . . . . . 13
⊢ (𝐴 ∩ 𝑦) ∈ V | 
| 126 | 125 | dfiun3 5979 | . . . . . . . . . . . 12
⊢ ∪ 𝑦 ∈ 𝑥 (𝐴 ∩ 𝑦) = ∪ ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) | 
| 127 | 123, 126 | eqtr3i 2766 | . . . . . . . . . . 11
⊢ (𝐴 ∩ ∪ 𝑥) =
∪ ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) | 
| 128 |  | simplr 768 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → 𝑡 ∈ 𝐿) | 
| 129 |  | nfv 1913 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑦(𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) | 
| 130 |  | nfv 1913 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑦 𝑥 ≼
ω | 
| 131 |  | nfdisj1 5123 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑦Disj
𝑦 ∈ 𝑥 𝑦 | 
| 132 | 130, 131 | nfan 1898 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑦(𝑥 ≼ ω ∧
Disj 𝑦 ∈ 𝑥 𝑦) | 
| 133 | 129, 132 | nfan 1898 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑦((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) | 
| 134 |  | nfv 1913 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑦 𝑡 ∈ 𝐿 | 
| 135 | 133, 134 | nfan 1898 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑦(((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ 𝑡 ∈ 𝐿) | 
| 136 |  | nfv 1913 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑦 𝑇 ⊆ 𝑡 | 
| 137 | 135, 136 | nfan 1898 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦((((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) | 
| 138 |  | elpwi 4606 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} → 𝑥 ⊆ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) | 
| 139 | 138 | ad4antlr 733 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → 𝑥 ⊆ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) | 
| 140 | 139 | sselda 3982 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) | 
| 141 |  | ineq2 4213 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 = 𝑦 → (𝐴 ∩ 𝑏) = (𝐴 ∩ 𝑦)) | 
| 142 | 141 | eleq1d 2825 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = 𝑦 → ((𝐴 ∩ 𝑏) ∈ 𝐸 ↔ (𝐴 ∩ 𝑦) ∈ 𝐸)) | 
| 143 | 142 | elrab 3691 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ↔ (𝑦 ∈ 𝒫 𝑂 ∧ (𝐴 ∩ 𝑦) ∈ 𝐸)) | 
| 144 | 143 | simprbi 496 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} → (𝐴 ∩ 𝑦) ∈ 𝐸) | 
| 145 | 140, 144 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) ∧ 𝑦 ∈ 𝑥) → (𝐴 ∩ 𝑦) ∈ 𝐸) | 
| 146 |  | simpllr 775 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) ∧ 𝑦 ∈ 𝑥) → 𝑡 ∈ 𝐿) | 
| 147 |  | simplr 768 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) ∧ 𝑦 ∈ 𝑥) → 𝑇 ⊆ 𝑡) | 
| 148 | 23 | eleq2i 2832 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∩ 𝑦) ∈ 𝐸 ↔ (𝐴 ∩ 𝑦) ∈ ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡}) | 
| 149 | 125 | elintrab 4959 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∩ 𝑦) ∈ ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡} ↔ ∀𝑡 ∈ 𝐿 (𝑇 ⊆ 𝑡 → (𝐴 ∩ 𝑦) ∈ 𝑡)) | 
| 150 | 148, 149 | bitri 275 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∩ 𝑦) ∈ 𝐸 ↔ ∀𝑡 ∈ 𝐿 (𝑇 ⊆ 𝑡 → (𝐴 ∩ 𝑦) ∈ 𝑡)) | 
| 151 |  | rspa 3247 | . . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑡 ∈
𝐿 (𝑇 ⊆ 𝑡 → (𝐴 ∩ 𝑦) ∈ 𝑡) ∧ 𝑡 ∈ 𝐿) → (𝑇 ⊆ 𝑡 → (𝐴 ∩ 𝑦) ∈ 𝑡)) | 
| 152 | 150, 151 | sylanb 581 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∩ 𝑦) ∈ 𝐸 ∧ 𝑡 ∈ 𝐿) → (𝑇 ⊆ 𝑡 → (𝐴 ∩ 𝑦) ∈ 𝑡)) | 
| 153 | 152 | imp 406 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∩ 𝑦) ∈ 𝐸 ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → (𝐴 ∩ 𝑦) ∈ 𝑡) | 
| 154 | 145, 146,
147, 153 | syl21anc 837 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) ∧ 𝑦 ∈ 𝑥) → (𝐴 ∩ 𝑦) ∈ 𝑡) | 
| 155 | 154 | ex 412 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → (𝑦 ∈ 𝑥 → (𝐴 ∩ 𝑦) ∈ 𝑡)) | 
| 156 | 137, 155 | ralrimi 3256 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → ∀𝑦 ∈ 𝑥 (𝐴 ∩ 𝑦) ∈ 𝑡) | 
| 157 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) = (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) | 
| 158 | 157 | rnmptss 7142 | . . . . . . . . . . . . . 14
⊢
(∀𝑦 ∈
𝑥 (𝐴 ∩ 𝑦) ∈ 𝑡 → ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) ⊆ 𝑡) | 
| 159 | 156, 158 | syl 17 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) ⊆ 𝑡) | 
| 160 | 128, 159 | sselpwd 5327 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) ∈ 𝒫 𝑡) | 
| 161 |  | simpllr 775 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) | 
| 162 | 161 | simpld 494 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → 𝑥 ≼ ω) | 
| 163 |  | 1stcrestlem 23461 | . . . . . . . . . . . . 13
⊢ (𝑥 ≼ ω → ran
(𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) ≼ ω) | 
| 164 | 162, 163 | syl 17 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) ≼ ω) | 
| 165 | 161 | simprd 495 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → Disj 𝑦 ∈ 𝑥 𝑦) | 
| 166 |  | disjin2 32601 | . . . . . . . . . . . . . 14
⊢
(Disj 𝑦
∈ 𝑥 𝑦 → Disj 𝑦 ∈ 𝑥 (𝐴 ∩ 𝑦)) | 
| 167 |  | disjrnmpt 32599 | . . . . . . . . . . . . . 14
⊢
(Disj 𝑦
∈ 𝑥 (𝐴 ∩ 𝑦) → Disj 𝑧 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦))𝑧) | 
| 168 | 165, 166,
167 | 3syl 18 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → Disj 𝑧 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦))𝑧) | 
| 169 |  | nfmpt1 5249 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦(𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) | 
| 170 | 169 | nfrn 5962 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑦ran
(𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) | 
| 171 |  | nfcv 2904 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑧𝑦 | 
| 172 |  | nfcv 2904 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑦𝑧 | 
| 173 |  | id 22 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧) | 
| 174 | 170, 171,
172, 173 | cbvdisjf 32585 | . . . . . . . . . . . . 13
⊢
(Disj 𝑦
∈ ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦))𝑦 ↔ Disj 𝑧 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦))𝑧) | 
| 175 | 168, 174 | sylibr 234 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → Disj 𝑦 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦))𝑦) | 
| 176 |  | breq1 5145 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 = ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) → (𝑧 ≼ ω ↔ ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) ≼ ω)) | 
| 177 | 172, 170 | disjeq1f 32587 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 = ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) → (Disj 𝑦 ∈ 𝑧 𝑦 ↔ Disj 𝑦 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦))𝑦)) | 
| 178 | 176, 177 | anbi12d 632 | . . . . . . . . . . . . . . 15
⊢ (𝑧 = ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) → ((𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦) ↔ (ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦))𝑦))) | 
| 179 |  | unieq 4917 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 = ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) → ∪ 𝑧 = ∪
ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦))) | 
| 180 | 179 | eleq1d 2825 | . . . . . . . . . . . . . . 15
⊢ (𝑧 = ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) → (∪ 𝑧 ∈ 𝑡 ↔ ∪ ran
(𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) ∈ 𝑡)) | 
| 181 | 178, 180 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢ (𝑧 = ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) → (((𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦) → ∪ 𝑧 ∈ 𝑡) ↔ ((ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦))𝑦) → ∪ ran
(𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) ∈ 𝑡))) | 
| 182 | 14 | simp3d 1144 | . . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ 𝐿 → ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑡)) | 
| 183 |  | breq1 5145 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑧 → (𝑥 ≼ ω ↔ 𝑧 ≼ ω)) | 
| 184 |  | disjeq1 5116 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑧 → (Disj 𝑦 ∈ 𝑥 𝑦 ↔ Disj 𝑦 ∈ 𝑧 𝑦)) | 
| 185 | 183, 184 | anbi12d 632 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑧 → ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) ↔ (𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦))) | 
| 186 |  | unieq 4917 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑧 → ∪ 𝑥 = ∪
𝑧) | 
| 187 | 186 | eleq1d 2825 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑧 → (∪ 𝑥 ∈ 𝑡 ↔ ∪ 𝑧 ∈ 𝑡)) | 
| 188 | 185, 187 | imbi12d 344 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → (((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑡) ↔ ((𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦) → ∪ 𝑧 ∈ 𝑡))) | 
| 189 | 188 | cbvralvw 3236 | . . . . . . . . . . . . . . . 16
⊢
(∀𝑥 ∈
𝒫 𝑡((𝑥 ≼ ω ∧
Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑡) ↔ ∀𝑧 ∈ 𝒫 𝑡((𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦) → ∪ 𝑧 ∈ 𝑡)) | 
| 190 | 182, 189 | sylib 218 | . . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ 𝐿 → ∀𝑧 ∈ 𝒫 𝑡((𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦) → ∪ 𝑧 ∈ 𝑡)) | 
| 191 | 190 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ 𝐿 ∧ ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) ∈ 𝒫 𝑡) → ∀𝑧 ∈ 𝒫 𝑡((𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦) → ∪ 𝑧 ∈ 𝑡)) | 
| 192 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ 𝐿 ∧ ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) ∈ 𝒫 𝑡) → ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) ∈ 𝒫 𝑡) | 
| 193 | 181, 191,
192 | rspcdva 3622 | . . . . . . . . . . . . 13
⊢ ((𝑡 ∈ 𝐿 ∧ ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) ∈ 𝒫 𝑡) → ((ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦))𝑦) → ∪ ran
(𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) ∈ 𝑡)) | 
| 194 | 193 | imp 406 | . . . . . . . . . . . 12
⊢ (((𝑡 ∈ 𝐿 ∧ ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) ∈ 𝒫 𝑡) ∧ (ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦))𝑦)) → ∪ ran
(𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) ∈ 𝑡) | 
| 195 | 128, 160,
164, 175, 194 | syl22anc 838 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → ∪ ran
(𝑦 ∈ 𝑥 ↦ (𝐴 ∩ 𝑦)) ∈ 𝑡) | 
| 196 | 127, 195 | eqeltrid 2844 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ 𝑡 ∈ 𝐿) ∧ 𝑇 ⊆ 𝑡) → (𝐴 ∩ ∪ 𝑥) ∈ 𝑡) | 
| 197 | 196 | ex 412 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ 𝑡 ∈ 𝐿) → (𝑇 ⊆ 𝑡 → (𝐴 ∩ ∪ 𝑥) ∈ 𝑡)) | 
| 198 | 197 | ralrimiva 3145 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → ∀𝑡 ∈ 𝐿 (𝑇 ⊆ 𝑡 → (𝐴 ∩ ∪ 𝑥) ∈ 𝑡)) | 
| 199 |  | vuniex 7760 | . . . . . . . . . 10
⊢ ∪ 𝑥
∈ V | 
| 200 | 199 | inex2 5317 | . . . . . . . . 9
⊢ (𝐴 ∩ ∪ 𝑥)
∈ V | 
| 201 | 200 | elintrab 4959 | . . . . . . . 8
⊢ ((𝐴 ∩ ∪ 𝑥)
∈ ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡} ↔ ∀𝑡 ∈ 𝐿 (𝑇 ⊆ 𝑡 → (𝐴 ∩ ∪ 𝑥) ∈ 𝑡)) | 
| 202 | 198, 201 | sylibr 234 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → (𝐴 ∩ ∪ 𝑥) ∈ ∩ {𝑡
∈ 𝐿 ∣ 𝑇 ⊆ 𝑡}) | 
| 203 | 202, 23 | eleqtrrdi 2851 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → (𝐴 ∩ ∪ 𝑥) ∈ 𝐸) | 
| 204 | 118, 122,
203 | elrabd 3693 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → ∪ 𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) | 
| 205 | 204 | ex 412 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) → ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸})) | 
| 206 | 205 | ralrimiva 3145 | . . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸})) | 
| 207 | 25, 116, 206 | 3jca 1128 | . 2
⊢ (𝜑 → (∅ ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ∧ ∀𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} (𝑂 ∖ 𝑥) ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ∧ ∀𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}))) | 
| 208 | 12 | isldsys 34158 | . 2
⊢ ({𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ∈ 𝐿 ↔ ({𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ∈ 𝒫 𝒫 𝑂 ∧ (∅ ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ∧ ∀𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} (𝑂 ∖ 𝑥) ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ∧ ∀𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸})))) | 
| 209 | 7, 207, 208 | sylanbrc 583 | 1
⊢ (𝜑 → {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ∈ 𝐿) |