| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dfiin2g 5032 | . . 3
⊢
(∀𝑦 ∈
𝐼 𝑆 ∈ 𝐶 → ∩
𝑦 ∈ 𝐼 𝑆 = ∩ {𝑠 ∣ ∃𝑦 ∈ 𝐼 𝑠 = 𝑆}) | 
| 2 | 1 | 3ad2ant3 1136 | . 2
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐼 ≠ ∅ ∧ ∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶) → ∩
𝑦 ∈ 𝐼 𝑆 = ∩ {𝑠 ∣ ∃𝑦 ∈ 𝐼 𝑠 = 𝑆}) | 
| 3 |  | simp1 1137 | . . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐼 ≠ ∅ ∧ ∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶) → 𝐶 ∈ (Moore‘𝑋)) | 
| 4 |  | uniiunlem 4087 | . . . . 5
⊢
(∀𝑦 ∈
𝐼 𝑆 ∈ 𝐶 → (∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 ↔ {𝑠 ∣ ∃𝑦 ∈ 𝐼 𝑠 = 𝑆} ⊆ 𝐶)) | 
| 5 | 4 | ibi 267 | . . . 4
⊢
(∀𝑦 ∈
𝐼 𝑆 ∈ 𝐶 → {𝑠 ∣ ∃𝑦 ∈ 𝐼 𝑠 = 𝑆} ⊆ 𝐶) | 
| 6 | 5 | 3ad2ant3 1136 | . . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐼 ≠ ∅ ∧ ∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶) → {𝑠 ∣ ∃𝑦 ∈ 𝐼 𝑠 = 𝑆} ⊆ 𝐶) | 
| 7 |  | n0 4353 | . . . . . 6
⊢ (𝐼 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝐼) | 
| 8 |  | nfra1 3284 | . . . . . . . 8
⊢
Ⅎ𝑦∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 | 
| 9 |  | nfre1 3285 | . . . . . . . . . 10
⊢
Ⅎ𝑦∃𝑦 ∈ 𝐼 𝑠 = 𝑆 | 
| 10 | 9 | nfab 2911 | . . . . . . . . 9
⊢
Ⅎ𝑦{𝑠 ∣ ∃𝑦 ∈ 𝐼 𝑠 = 𝑆} | 
| 11 |  | nfcv 2905 | . . . . . . . . 9
⊢
Ⅎ𝑦∅ | 
| 12 | 10, 11 | nfne 3043 | . . . . . . . 8
⊢
Ⅎ𝑦{𝑠 ∣ ∃𝑦 ∈ 𝐼 𝑠 = 𝑆} ≠ ∅ | 
| 13 | 8, 12 | nfim 1896 | . . . . . . 7
⊢
Ⅎ𝑦(∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 → {𝑠 ∣ ∃𝑦 ∈ 𝐼 𝑠 = 𝑆} ≠ ∅) | 
| 14 |  | rsp 3247 | . . . . . . . . . 10
⊢
(∀𝑦 ∈
𝐼 𝑆 ∈ 𝐶 → (𝑦 ∈ 𝐼 → 𝑆 ∈ 𝐶)) | 
| 15 | 14 | com12 32 | . . . . . . . . 9
⊢ (𝑦 ∈ 𝐼 → (∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 → 𝑆 ∈ 𝐶)) | 
| 16 |  | elisset 2823 | . . . . . . . . . . 11
⊢ (𝑆 ∈ 𝐶 → ∃𝑠 𝑠 = 𝑆) | 
| 17 |  | rspe 3249 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝐼 ∧ ∃𝑠 𝑠 = 𝑆) → ∃𝑦 ∈ 𝐼 ∃𝑠 𝑠 = 𝑆) | 
| 18 | 17 | ex 412 | . . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐼 → (∃𝑠 𝑠 = 𝑆 → ∃𝑦 ∈ 𝐼 ∃𝑠 𝑠 = 𝑆)) | 
| 19 | 16, 18 | syl5 34 | . . . . . . . . . 10
⊢ (𝑦 ∈ 𝐼 → (𝑆 ∈ 𝐶 → ∃𝑦 ∈ 𝐼 ∃𝑠 𝑠 = 𝑆)) | 
| 20 |  | rexcom4 3288 | . . . . . . . . . 10
⊢
(∃𝑦 ∈
𝐼 ∃𝑠 𝑠 = 𝑆 ↔ ∃𝑠∃𝑦 ∈ 𝐼 𝑠 = 𝑆) | 
| 21 | 19, 20 | imbitrdi 251 | . . . . . . . . 9
⊢ (𝑦 ∈ 𝐼 → (𝑆 ∈ 𝐶 → ∃𝑠∃𝑦 ∈ 𝐼 𝑠 = 𝑆)) | 
| 22 | 15, 21 | syld 47 | . . . . . . . 8
⊢ (𝑦 ∈ 𝐼 → (∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 → ∃𝑠∃𝑦 ∈ 𝐼 𝑠 = 𝑆)) | 
| 23 |  | abn0 4385 | . . . . . . . 8
⊢ ({𝑠 ∣ ∃𝑦 ∈ 𝐼 𝑠 = 𝑆} ≠ ∅ ↔ ∃𝑠∃𝑦 ∈ 𝐼 𝑠 = 𝑆) | 
| 24 | 22, 23 | imbitrrdi 252 | . . . . . . 7
⊢ (𝑦 ∈ 𝐼 → (∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 → {𝑠 ∣ ∃𝑦 ∈ 𝐼 𝑠 = 𝑆} ≠ ∅)) | 
| 25 | 13, 24 | exlimi 2217 | . . . . . 6
⊢
(∃𝑦 𝑦 ∈ 𝐼 → (∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 → {𝑠 ∣ ∃𝑦 ∈ 𝐼 𝑠 = 𝑆} ≠ ∅)) | 
| 26 | 7, 25 | sylbi 217 | . . . . 5
⊢ (𝐼 ≠ ∅ →
(∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 → {𝑠 ∣ ∃𝑦 ∈ 𝐼 𝑠 = 𝑆} ≠ ∅)) | 
| 27 | 26 | imp 406 | . . . 4
⊢ ((𝐼 ≠ ∅ ∧
∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶) → {𝑠 ∣ ∃𝑦 ∈ 𝐼 𝑠 = 𝑆} ≠ ∅) | 
| 28 | 27 | 3adant1 1131 | . . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐼 ≠ ∅ ∧ ∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶) → {𝑠 ∣ ∃𝑦 ∈ 𝐼 𝑠 = 𝑆} ≠ ∅) | 
| 29 |  | mreintcl 17638 | . . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ {𝑠 ∣ ∃𝑦 ∈ 𝐼 𝑠 = 𝑆} ⊆ 𝐶 ∧ {𝑠 ∣ ∃𝑦 ∈ 𝐼 𝑠 = 𝑆} ≠ ∅) → ∩ {𝑠
∣ ∃𝑦 ∈
𝐼 𝑠 = 𝑆} ∈ 𝐶) | 
| 30 | 3, 6, 28, 29 | syl3anc 1373 | . 2
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐼 ≠ ∅ ∧ ∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶) → ∩ {𝑠 ∣ ∃𝑦 ∈ 𝐼 𝑠 = 𝑆} ∈ 𝐶) | 
| 31 | 2, 30 | eqeltrd 2841 | 1
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐼 ≠ ∅ ∧ ∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶) → ∩
𝑦 ∈ 𝐼 𝑆 ∈ 𝐶) |