Proof of Theorem fin23lem29
Step | Hyp | Ref
| Expression |
1 | | fin23lem.e |
. 2
⊢ 𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄)) |
2 | | eqif 4506 |
. . 3
⊢ (𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄)) ↔ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄)))) |
3 | 2 | biimpi 215 |
. 2
⊢ (𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄)) → ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄)))) |
4 | | rneq 5844 |
. . . . . 6
⊢ (𝑍 = (𝑡 ∘ 𝑅) → ran 𝑍 = ran (𝑡 ∘ 𝑅)) |
5 | 4 | unieqd 4859 |
. . . . 5
⊢ (𝑍 = (𝑡 ∘ 𝑅) → ∪ ran
𝑍 = ∪ ran (𝑡 ∘ 𝑅)) |
6 | | rncoss 5880 |
. . . . . 6
⊢ ran
(𝑡 ∘ 𝑅) ⊆ ran 𝑡 |
7 | 6 | unissi 4854 |
. . . . 5
⊢ ∪ ran (𝑡 ∘ 𝑅) ⊆ ∪ ran
𝑡 |
8 | 5, 7 | eqsstrdi 3980 |
. . . 4
⊢ (𝑍 = (𝑡 ∘ 𝑅) → ∪ ran
𝑍 ⊆ ∪ ran 𝑡) |
9 | 8 | adantl 482 |
. . 3
⊢ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) → ∪ ran
𝑍 ⊆ ∪ ran 𝑡) |
10 | | rneq 5844 |
. . . . . 6
⊢ (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄) → ran 𝑍 = ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄)) |
11 | 10 | unieqd 4859 |
. . . . 5
⊢ (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄) → ∪ ran 𝑍 = ∪ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄)) |
12 | | rncoss 5880 |
. . . . . . 7
⊢ ran
((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄) ⊆ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) |
13 | 12 | unissi 4854 |
. . . . . 6
⊢ ∪ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄) ⊆ ∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) |
14 | | unissb 4879 |
. . . . . . 7
⊢ (∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ⊆ ∪ ran 𝑡 ↔ ∀𝑎 ∈ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈))𝑎 ⊆ ∪ ran
𝑡) |
15 | | abid 2721 |
. . . . . . . . 9
⊢ (𝑎 ∈ {𝑎 ∣ ∃𝑧 ∈ 𝑃 𝑎 = ((𝑡‘𝑧) ∖ ∩ ran
𝑈)} ↔ ∃𝑧 ∈ 𝑃 𝑎 = ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) |
16 | | fvssunirn 6800 |
. . . . . . . . . . . . 13
⊢ (𝑡‘𝑧) ⊆ ∪ ran
𝑡 |
17 | 16 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑃 → (𝑡‘𝑧) ⊆ ∪ ran
𝑡) |
18 | 17 | ssdifssd 4082 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑃 → ((𝑡‘𝑧) ∖ ∩ ran
𝑈) ⊆ ∪ ran 𝑡) |
19 | | sseq1 3951 |
. . . . . . . . . . 11
⊢ (𝑎 = ((𝑡‘𝑧) ∖ ∩ ran
𝑈) → (𝑎 ⊆ ∪ ran 𝑡 ↔ ((𝑡‘𝑧) ∖ ∩ ran
𝑈) ⊆ ∪ ran 𝑡)) |
20 | 18, 19 | syl5ibrcom 246 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑃 → (𝑎 = ((𝑡‘𝑧) ∖ ∩ ran
𝑈) → 𝑎 ⊆ ∪ ran 𝑡)) |
21 | 20 | rexlimiv 3211 |
. . . . . . . . 9
⊢
(∃𝑧 ∈
𝑃 𝑎 = ((𝑡‘𝑧) ∖ ∩ ran
𝑈) → 𝑎 ⊆ ∪ ran 𝑡) |
22 | 15, 21 | sylbi 216 |
. . . . . . . 8
⊢ (𝑎 ∈ {𝑎 ∣ ∃𝑧 ∈ 𝑃 𝑎 = ((𝑡‘𝑧) ∖ ∩ ran
𝑈)} → 𝑎 ⊆ ∪ ran 𝑡) |
23 | | eqid 2740 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) = (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) |
24 | 23 | rnmpt 5863 |
. . . . . . . 8
⊢ ran
(𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) = {𝑎 ∣ ∃𝑧 ∈ 𝑃 𝑎 = ((𝑡‘𝑧) ∖ ∩ ran
𝑈)} |
25 | 22, 24 | eleq2s 2859 |
. . . . . . 7
⊢ (𝑎 ∈ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) → 𝑎 ⊆ ∪ ran 𝑡) |
26 | 14, 25 | mprgbir 3081 |
. . . . . 6
⊢ ∪ ran (𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ⊆ ∪ ran 𝑡 |
27 | 13, 26 | sstri 3935 |
. . . . 5
⊢ ∪ ran ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄) ⊆ ∪ ran 𝑡 |
28 | 11, 27 | eqsstrdi 3980 |
. . . 4
⊢ (𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄) → ∪ ran 𝑍 ⊆ ∪ ran
𝑡) |
29 | 28 | adantl 482 |
. . 3
⊢ ((¬
𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄)) → ∪ ran 𝑍 ⊆ ∪ ran
𝑡) |
30 | 9, 29 | jaoi 854 |
. 2
⊢ (((𝑃 ∈ Fin ∧ 𝑍 = (𝑡 ∘ 𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄))) → ∪ ran 𝑍 ⊆ ∪ ran
𝑡) |
31 | 1, 3, 30 | mp2b 10 |
1
⊢ ∪ ran 𝑍 ⊆ ∪ ran
𝑡 |