Proof of Theorem fin23lem29
| Step | Hyp | Ref
| Expression |
| 1 | | fin23lem.e |
. 2
⊢ 𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄)) |
| 2 | | eqif 4567 |
. . 3
⊢ (𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄)) ↔ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄)))) |
| 3 | 2 | biimpi 216 |
. 2
⊢ (𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄)) → ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄)))) |
| 4 | | rneq 5947 |
. . . . . 6
⊢ (𝑍 = (𝑡 ∘ 𝑅) → ran 𝑍 = ran (𝑡 ∘ 𝑅)) |
| 5 | 4 | unieqd 4920 |
. . . . 5
⊢ (𝑍 = (𝑡 ∘ 𝑅) → ∪ ran
𝑍 = ∪ ran (𝑡 ∘ 𝑅)) |
| 6 | | rncoss 5986 |
. . . . . 6
⊢ ran
(𝑡 ∘ 𝑅) ⊆ ran 𝑡 |
| 7 | 6 | unissi 4916 |
. . . . 5
⊢ ∪ ran (𝑡 ∘ 𝑅) ⊆ ∪ ran
𝑡 |
| 8 | 5, 7 | eqsstrdi 4028 |
. . . 4
⊢ (𝑍 = (𝑡 ∘ 𝑅) → ∪ ran
𝑍 ⊆ ∪ ran 𝑡) |
| 9 | 8 | adantl 481 |
. . 3
⊢ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) → ∪ ran
𝑍 ⊆ ∪ ran 𝑡) |
| 10 | | rneq 5947 |
. . . . . 6
⊢ (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄) → ran 𝑍 = ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄)) |
| 11 | 10 | unieqd 4920 |
. . . . 5
⊢ (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄) → ∪ ran 𝑍 = ∪ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄)) |
| 12 | | rncoss 5986 |
. . . . . . 7
⊢ ran
((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄) ⊆ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) |
| 13 | 12 | unissi 4916 |
. . . . . 6
⊢ ∪ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄) ⊆ ∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) |
| 14 | | unissb 4939 |
. . . . . . 7
⊢ (∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ⊆ ∪ ran 𝑡 ↔ ∀𝑎 ∈ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈))𝑎 ⊆ ∪ ran
𝑡) |
| 15 | | abid 2718 |
. . . . . . . . 9
⊢ (𝑎 ∈ {𝑎 ∣ ∃𝑧 ∈ 𝑃 𝑎 = ((𝑡‘𝑧) ∖ ∩ ran
𝑈)} ↔ ∃𝑧 ∈ 𝑃 𝑎 = ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) |
| 16 | | fvssunirn 6939 |
. . . . . . . . . . . . 13
⊢ (𝑡‘𝑧) ⊆ ∪ ran
𝑡 |
| 17 | 16 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑃 → (𝑡‘𝑧) ⊆ ∪ ran
𝑡) |
| 18 | 17 | ssdifssd 4147 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑃 → ((𝑡‘𝑧) ∖ ∩ ran
𝑈) ⊆ ∪ ran 𝑡) |
| 19 | | sseq1 4009 |
. . . . . . . . . . 11
⊢ (𝑎 = ((𝑡‘𝑧) ∖ ∩ ran
𝑈) → (𝑎 ⊆ ∪ ran 𝑡 ↔ ((𝑡‘𝑧) ∖ ∩ ran
𝑈) ⊆ ∪ ran 𝑡)) |
| 20 | 18, 19 | syl5ibrcom 247 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑃 → (𝑎 = ((𝑡‘𝑧) ∖ ∩ ran
𝑈) → 𝑎 ⊆ ∪ ran 𝑡)) |
| 21 | 20 | rexlimiv 3148 |
. . . . . . . . 9
⊢
(∃𝑧 ∈
𝑃 𝑎 = ((𝑡‘𝑧) ∖ ∩ ran
𝑈) → 𝑎 ⊆ ∪ ran 𝑡) |
| 22 | 15, 21 | sylbi 217 |
. . . . . . . 8
⊢ (𝑎 ∈ {𝑎 ∣ ∃𝑧 ∈ 𝑃 𝑎 = ((𝑡‘𝑧) ∖ ∩ ran
𝑈)} → 𝑎 ⊆ ∪ ran 𝑡) |
| 23 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) = (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) |
| 24 | 23 | rnmpt 5968 |
. . . . . . . 8
⊢ ran
(𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) = {𝑎 ∣ ∃𝑧 ∈ 𝑃 𝑎 = ((𝑡‘𝑧) ∖ ∩ ran
𝑈)} |
| 25 | 22, 24 | eleq2s 2859 |
. . . . . . 7
⊢ (𝑎 ∈ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) → 𝑎 ⊆ ∪ ran 𝑡) |
| 26 | 14, 25 | mprgbir 3068 |
. . . . . 6
⊢ ∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ⊆ ∪ ran 𝑡 |
| 27 | 13, 26 | sstri 3993 |
. . . . 5
⊢ ∪ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄) ⊆ ∪ ran 𝑡 |
| 28 | 11, 27 | eqsstrdi 4028 |
. . . 4
⊢ (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄) → ∪ ran 𝑍 ⊆ ∪ ran
𝑡) |
| 29 | 28 | adantl 481 |
. . 3
⊢ ((¬
𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄)) → ∪ ran 𝑍 ⊆ ∪ ran
𝑡) |
| 30 | 9, 29 | jaoi 858 |
. 2
⊢ (((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄))) → ∪ ran 𝑍 ⊆ ∪ ran
𝑡) |
| 31 | 1, 3, 30 | mp2b 10 |
1
⊢ ∪ ran 𝑍 ⊆ ∪ ran
𝑡 |