Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → 𝐶 ∈ (Moore‘𝑋)) |
2 | | simpll 790 |
. . . . . . 7
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) ∧ 𝑠 ∈ 𝑈) → 𝐶 ∈ (Moore‘𝑋)) |
3 | | ssel2 3598 |
. . . . . . . . 9
⊢ ((𝑈 ⊆ 𝒫 𝑋 ∧ 𝑠 ∈ 𝑈) → 𝑠 ∈ 𝒫 𝑋) |
4 | 3 | elpwid 4170 |
. . . . . . . 8
⊢ ((𝑈 ⊆ 𝒫 𝑋 ∧ 𝑠 ∈ 𝑈) → 𝑠 ⊆ 𝑋) |
5 | 4 | adantll 750 |
. . . . . . 7
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) ∧ 𝑠 ∈ 𝑈) → 𝑠 ⊆ 𝑋) |
6 | | mrcfval.f |
. . . . . . . 8
⊢ 𝐹 = (mrCls‘𝐶) |
7 | 6 | mrcssid 16277 |
. . . . . . 7
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠 ⊆ 𝑋) → 𝑠 ⊆ (𝐹‘𝑠)) |
8 | 2, 5, 7 | syl2anc 693 |
. . . . . 6
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) ∧ 𝑠 ∈ 𝑈) → 𝑠 ⊆ (𝐹‘𝑠)) |
9 | 6 | mrcf 16269 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋⟶𝐶) |
10 | | ffun 6048 |
. . . . . . . . . . 11
⊢ (𝐹:𝒫 𝑋⟶𝐶 → Fun 𝐹) |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (Moore‘𝑋) → Fun 𝐹) |
12 | 11 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → Fun 𝐹) |
13 | | fdm 6051 |
. . . . . . . . . . . 12
⊢ (𝐹:𝒫 𝑋⟶𝐶 → dom 𝐹 = 𝒫 𝑋) |
14 | 9, 13 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (Moore‘𝑋) → dom 𝐹 = 𝒫 𝑋) |
15 | 14 | sseq2d 3633 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (Moore‘𝑋) → (𝑈 ⊆ dom 𝐹 ↔ 𝑈 ⊆ 𝒫 𝑋)) |
16 | 15 | biimpar 502 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → 𝑈 ⊆ dom 𝐹) |
17 | | funfvima2 6493 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑈 ⊆ dom 𝐹) → (𝑠 ∈ 𝑈 → (𝐹‘𝑠) ∈ (𝐹 “ 𝑈))) |
18 | 12, 16, 17 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → (𝑠 ∈ 𝑈 → (𝐹‘𝑠) ∈ (𝐹 “ 𝑈))) |
19 | 18 | imp 445 |
. . . . . . 7
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) ∧ 𝑠 ∈ 𝑈) → (𝐹‘𝑠) ∈ (𝐹 “ 𝑈)) |
20 | | elssuni 4467 |
. . . . . . 7
⊢ ((𝐹‘𝑠) ∈ (𝐹 “ 𝑈) → (𝐹‘𝑠) ⊆ ∪ (𝐹 “ 𝑈)) |
21 | 19, 20 | syl 17 |
. . . . . 6
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) ∧ 𝑠 ∈ 𝑈) → (𝐹‘𝑠) ⊆ ∪ (𝐹 “ 𝑈)) |
22 | 8, 21 | sstrd 3613 |
. . . . 5
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) ∧ 𝑠 ∈ 𝑈) → 𝑠 ⊆ ∪ (𝐹 “ 𝑈)) |
23 | 22 | ralrimiva 2966 |
. . . 4
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → ∀𝑠 ∈ 𝑈 𝑠 ⊆ ∪ (𝐹 “ 𝑈)) |
24 | | unissb 4469 |
. . . 4
⊢ (∪ 𝑈
⊆ ∪ (𝐹 “ 𝑈) ↔ ∀𝑠 ∈ 𝑈 𝑠 ⊆ ∪ (𝐹 “ 𝑈)) |
25 | 23, 24 | sylibr 224 |
. . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → ∪ 𝑈 ⊆ ∪ (𝐹
“ 𝑈)) |
26 | 6 | mrcssv 16274 |
. . . . . . 7
⊢ (𝐶 ∈ (Moore‘𝑋) → (𝐹‘𝑥) ⊆ 𝑋) |
27 | 26 | adantr 481 |
. . . . . 6
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → (𝐹‘𝑥) ⊆ 𝑋) |
28 | 27 | ralrimivw 2967 |
. . . . 5
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → ∀𝑥 ∈ 𝑈 (𝐹‘𝑥) ⊆ 𝑋) |
29 | | ffn 6045 |
. . . . . . 7
⊢ (𝐹:𝒫 𝑋⟶𝐶 → 𝐹 Fn 𝒫 𝑋) |
30 | 9, 29 | syl 17 |
. . . . . 6
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹 Fn 𝒫 𝑋) |
31 | | sseq1 3626 |
. . . . . . 7
⊢ (𝑠 = (𝐹‘𝑥) → (𝑠 ⊆ 𝑋 ↔ (𝐹‘𝑥) ⊆ 𝑋)) |
32 | 31 | ralima 6498 |
. . . . . 6
⊢ ((𝐹 Fn 𝒫 𝑋 ∧ 𝑈 ⊆ 𝒫 𝑋) → (∀𝑠 ∈ (𝐹 “ 𝑈)𝑠 ⊆ 𝑋 ↔ ∀𝑥 ∈ 𝑈 (𝐹‘𝑥) ⊆ 𝑋)) |
33 | 30, 32 | sylan 488 |
. . . . 5
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → (∀𝑠 ∈ (𝐹 “ 𝑈)𝑠 ⊆ 𝑋 ↔ ∀𝑥 ∈ 𝑈 (𝐹‘𝑥) ⊆ 𝑋)) |
34 | 28, 33 | mpbird 247 |
. . . 4
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → ∀𝑠 ∈ (𝐹 “ 𝑈)𝑠 ⊆ 𝑋) |
35 | | unissb 4469 |
. . . 4
⊢ (∪ (𝐹
“ 𝑈) ⊆ 𝑋 ↔ ∀𝑠 ∈ (𝐹 “ 𝑈)𝑠 ⊆ 𝑋) |
36 | 34, 35 | sylibr 224 |
. . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → ∪ (𝐹 “ 𝑈) ⊆ 𝑋) |
37 | 6 | mrcss 16276 |
. . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∪ 𝑈
⊆ ∪ (𝐹 “ 𝑈) ∧ ∪ (𝐹 “ 𝑈) ⊆ 𝑋) → (𝐹‘∪ 𝑈) ⊆ (𝐹‘∪ (𝐹 “ 𝑈))) |
38 | 1, 25, 36, 37 | syl3anc 1326 |
. 2
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → (𝐹‘∪ 𝑈) ⊆ (𝐹‘∪ (𝐹 “ 𝑈))) |
39 | | simpll 790 |
. . . . . . . 8
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ (Moore‘𝑋)) |
40 | | elssuni 4467 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑈 → 𝑥 ⊆ ∪ 𝑈) |
41 | 40 | adantl 482 |
. . . . . . . 8
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) ∧ 𝑥 ∈ 𝑈) → 𝑥 ⊆ ∪ 𝑈) |
42 | | sspwuni 4611 |
. . . . . . . . . . 11
⊢ (𝑈 ⊆ 𝒫 𝑋 ↔ ∪ 𝑈
⊆ 𝑋) |
43 | 42 | biimpi 206 |
. . . . . . . . . 10
⊢ (𝑈 ⊆ 𝒫 𝑋 → ∪ 𝑈
⊆ 𝑋) |
44 | 43 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → ∪ 𝑈 ⊆ 𝑋) |
45 | 44 | adantr 481 |
. . . . . . . 8
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) ∧ 𝑥 ∈ 𝑈) → ∪ 𝑈 ⊆ 𝑋) |
46 | 6 | mrcss 16276 |
. . . . . . . 8
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑥 ⊆ ∪ 𝑈 ∧ ∪ 𝑈
⊆ 𝑋) → (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑈)) |
47 | 39, 41, 45, 46 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) ∧ 𝑥 ∈ 𝑈) → (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑈)) |
48 | 47 | ralrimiva 2966 |
. . . . . 6
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → ∀𝑥 ∈ 𝑈 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑈)) |
49 | | sseq1 3626 |
. . . . . . . 8
⊢ (𝑠 = (𝐹‘𝑥) → (𝑠 ⊆ (𝐹‘∪ 𝑈) ↔ (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑈))) |
50 | 49 | ralima 6498 |
. . . . . . 7
⊢ ((𝐹 Fn 𝒫 𝑋 ∧ 𝑈 ⊆ 𝒫 𝑋) → (∀𝑠 ∈ (𝐹 “ 𝑈)𝑠 ⊆ (𝐹‘∪ 𝑈) ↔ ∀𝑥 ∈ 𝑈 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑈))) |
51 | 30, 50 | sylan 488 |
. . . . . 6
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → (∀𝑠 ∈ (𝐹 “ 𝑈)𝑠 ⊆ (𝐹‘∪ 𝑈) ↔ ∀𝑥 ∈ 𝑈 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑈))) |
52 | 48, 51 | mpbird 247 |
. . . . 5
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → ∀𝑠 ∈ (𝐹 “ 𝑈)𝑠 ⊆ (𝐹‘∪ 𝑈)) |
53 | | unissb 4469 |
. . . . 5
⊢ (∪ (𝐹
“ 𝑈) ⊆ (𝐹‘∪ 𝑈)
↔ ∀𝑠 ∈
(𝐹 “ 𝑈)𝑠 ⊆ (𝐹‘∪ 𝑈)) |
54 | 52, 53 | sylibr 224 |
. . . 4
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → ∪ (𝐹 “ 𝑈) ⊆ (𝐹‘∪ 𝑈)) |
55 | 6 | mrcssv 16274 |
. . . . 5
⊢ (𝐶 ∈ (Moore‘𝑋) → (𝐹‘∪ 𝑈) ⊆ 𝑋) |
56 | 55 | adantr 481 |
. . . 4
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → (𝐹‘∪ 𝑈) ⊆ 𝑋) |
57 | 6 | mrcss 16276 |
. . . 4
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∪ (𝐹
“ 𝑈) ⊆ (𝐹‘∪ 𝑈)
∧ (𝐹‘∪ 𝑈)
⊆ 𝑋) → (𝐹‘∪ (𝐹
“ 𝑈)) ⊆ (𝐹‘(𝐹‘∪ 𝑈))) |
58 | 1, 54, 56, 57 | syl3anc 1326 |
. . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → (𝐹‘∪ (𝐹 “ 𝑈)) ⊆ (𝐹‘(𝐹‘∪ 𝑈))) |
59 | 6 | mrcidm 16279 |
. . . 4
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∪ 𝑈
⊆ 𝑋) → (𝐹‘(𝐹‘∪ 𝑈)) = (𝐹‘∪ 𝑈)) |
60 | 1, 44, 59 | syl2anc 693 |
. . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → (𝐹‘(𝐹‘∪ 𝑈)) = (𝐹‘∪ 𝑈)) |
61 | 58, 60 | sseqtrd 3641 |
. 2
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → (𝐹‘∪ (𝐹 “ 𝑈)) ⊆ (𝐹‘∪ 𝑈)) |
62 | 38, 61 | eqssd 3620 |
1
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → (𝐹‘∪ 𝑈) = (𝐹‘∪ (𝐹 “ 𝑈))) |