Proof of Theorem mrcun
Step | Hyp | Ref
| Expression |
1 | | simp1 1061 |
. . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋) → 𝐶 ∈ (Moore‘𝑋)) |
2 | | mre1cl 16254 |
. . . . . . 7
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝑋 ∈ 𝐶) |
3 | | elpw2g 4827 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐶 → (𝑈 ∈ 𝒫 𝑋 ↔ 𝑈 ⊆ 𝑋)) |
4 | 2, 3 | syl 17 |
. . . . . 6
⊢ (𝐶 ∈ (Moore‘𝑋) → (𝑈 ∈ 𝒫 𝑋 ↔ 𝑈 ⊆ 𝑋)) |
5 | 4 | biimpar 502 |
. . . . 5
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → 𝑈 ∈ 𝒫 𝑋) |
6 | 5 | 3adant3 1081 |
. . . 4
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋) → 𝑈 ∈ 𝒫 𝑋) |
7 | | elpw2g 4827 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐶 → (𝑉 ∈ 𝒫 𝑋 ↔ 𝑉 ⊆ 𝑋)) |
8 | 2, 7 | syl 17 |
. . . . . 6
⊢ (𝐶 ∈ (Moore‘𝑋) → (𝑉 ∈ 𝒫 𝑋 ↔ 𝑉 ⊆ 𝑋)) |
9 | 8 | biimpar 502 |
. . . . 5
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑉 ⊆ 𝑋) → 𝑉 ∈ 𝒫 𝑋) |
10 | 9 | 3adant2 1080 |
. . . 4
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋) → 𝑉 ∈ 𝒫 𝑋) |
11 | | prssi 4353 |
. . . 4
⊢ ((𝑈 ∈ 𝒫 𝑋 ∧ 𝑉 ∈ 𝒫 𝑋) → {𝑈, 𝑉} ⊆ 𝒫 𝑋) |
12 | 6, 10, 11 | syl2anc 693 |
. . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋) → {𝑈, 𝑉} ⊆ 𝒫 𝑋) |
13 | | mrcfval.f |
. . . 4
⊢ 𝐹 = (mrCls‘𝐶) |
14 | 13 | mrcuni 16281 |
. . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ {𝑈, 𝑉} ⊆ 𝒫 𝑋) → (𝐹‘∪ {𝑈, 𝑉}) = (𝐹‘∪ (𝐹 “ {𝑈, 𝑉}))) |
15 | 1, 12, 14 | syl2anc 693 |
. 2
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋) → (𝐹‘∪ {𝑈, 𝑉}) = (𝐹‘∪ (𝐹 “ {𝑈, 𝑉}))) |
16 | | uniprg 4450 |
. . . 4
⊢ ((𝑈 ∈ 𝒫 𝑋 ∧ 𝑉 ∈ 𝒫 𝑋) → ∪ {𝑈, 𝑉} = (𝑈 ∪ 𝑉)) |
17 | 6, 10, 16 | syl2anc 693 |
. . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋) → ∪ {𝑈, 𝑉} = (𝑈 ∪ 𝑉)) |
18 | 17 | fveq2d 6195 |
. 2
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋) → (𝐹‘∪ {𝑈, 𝑉}) = (𝐹‘(𝑈 ∪ 𝑉))) |
19 | 13 | mrcf 16269 |
. . . . . . . 8
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋⟶𝐶) |
20 | | ffn 6045 |
. . . . . . . 8
⊢ (𝐹:𝒫 𝑋⟶𝐶 → 𝐹 Fn 𝒫 𝑋) |
21 | 19, 20 | syl 17 |
. . . . . . 7
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹 Fn 𝒫 𝑋) |
22 | 21 | 3ad2ant1 1082 |
. . . . . 6
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋) → 𝐹 Fn 𝒫 𝑋) |
23 | | fnimapr 6262 |
. . . . . 6
⊢ ((𝐹 Fn 𝒫 𝑋 ∧ 𝑈 ∈ 𝒫 𝑋 ∧ 𝑉 ∈ 𝒫 𝑋) → (𝐹 “ {𝑈, 𝑉}) = {(𝐹‘𝑈), (𝐹‘𝑉)}) |
24 | 22, 6, 10, 23 | syl3anc 1326 |
. . . . 5
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋) → (𝐹 “ {𝑈, 𝑉}) = {(𝐹‘𝑈), (𝐹‘𝑉)}) |
25 | 24 | unieqd 4446 |
. . . 4
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋) → ∪ (𝐹 “ {𝑈, 𝑉}) = ∪ {(𝐹‘𝑈), (𝐹‘𝑉)}) |
26 | | fvex 6201 |
. . . . 5
⊢ (𝐹‘𝑈) ∈ V |
27 | | fvex 6201 |
. . . . 5
⊢ (𝐹‘𝑉) ∈ V |
28 | 26, 27 | unipr 4449 |
. . . 4
⊢ ∪ {(𝐹‘𝑈), (𝐹‘𝑉)} = ((𝐹‘𝑈) ∪ (𝐹‘𝑉)) |
29 | 25, 28 | syl6eq 2672 |
. . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋) → ∪ (𝐹 “ {𝑈, 𝑉}) = ((𝐹‘𝑈) ∪ (𝐹‘𝑉))) |
30 | 29 | fveq2d 6195 |
. 2
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋) → (𝐹‘∪ (𝐹 “ {𝑈, 𝑉})) = (𝐹‘((𝐹‘𝑈) ∪ (𝐹‘𝑉)))) |
31 | 15, 18, 30 | 3eqtr3d 2664 |
1
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋) → (𝐹‘(𝑈 ∪ 𝑉)) = (𝐹‘((𝐹‘𝑈) ∪ (𝐹‘𝑉)))) |