Proof of Theorem fin23lem31
Step | Hyp | Ref
| Expression |
1 | | fin23lem17.f |
. . . 4
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran
𝑎 ∈ ran 𝑎)} |
2 | 1 | ssfin3ds 10086 |
. . 3
⊢ ((𝐺 ∈ 𝐹 ∧ ∪ ran
𝑡 ⊆ 𝐺) → ∪ ran
𝑡 ∈ 𝐹) |
3 | | fin23lem.a |
. . . . . 6
⊢ 𝑈 = seqω((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡) |
4 | | fin23lem.b |
. . . . . 6
⊢ 𝑃 = {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)} |
5 | | fin23lem.c |
. . . . . 6
⊢ 𝑄 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ 𝑃 (𝑥 ∩ 𝑃) ≈ 𝑤)) |
6 | | fin23lem.d |
. . . . . 6
⊢ 𝑅 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ (ω ∖ 𝑃)(𝑥 ∩ (ω ∖ 𝑃)) ≈ 𝑤)) |
7 | | fin23lem.e |
. . . . . 6
⊢ 𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄)) |
8 | 3, 1, 4, 5, 6, 7 | fin23lem29 10097 |
. . . . 5
⊢ ∪ ran 𝑍 ⊆ ∪ ran
𝑡 |
9 | 8 | a1i 11 |
. . . 4
⊢ ((𝑡:ω–1-1→𝑉 ∧ ∪ ran
𝑡 ∈ 𝐹) → ∪ ran
𝑍 ⊆ ∪ ran 𝑡) |
10 | 3, 1 | fin23lem21 10095 |
. . . . . . 7
⊢ ((∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡:ω–1-1→𝑉) → ∩ ran
𝑈 ≠
∅) |
11 | 10 | ancoms 459 |
. . . . . 6
⊢ ((𝑡:ω–1-1→𝑉 ∧ ∪ ran
𝑡 ∈ 𝐹) → ∩ ran
𝑈 ≠
∅) |
12 | | n0 4280 |
. . . . . 6
⊢ (∩ ran 𝑈 ≠ ∅ ↔ ∃𝑎 𝑎 ∈ ∩ ran
𝑈) |
13 | 11, 12 | sylib 217 |
. . . . 5
⊢ ((𝑡:ω–1-1→𝑉 ∧ ∪ ran
𝑡 ∈ 𝐹) → ∃𝑎 𝑎 ∈ ∩ ran
𝑈) |
14 | 3 | fnseqom 8286 |
. . . . . . . . . . . . 13
⊢ 𝑈 Fn ω |
15 | | fndm 6536 |
. . . . . . . . . . . . 13
⊢ (𝑈 Fn ω → dom 𝑈 = ω) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ dom 𝑈 = ω |
17 | | peano1 7735 |
. . . . . . . . . . . . 13
⊢ ∅
∈ ω |
18 | 17 | ne0ii 4271 |
. . . . . . . . . . . 12
⊢ ω
≠ ∅ |
19 | 16, 18 | eqnetri 3014 |
. . . . . . . . . . 11
⊢ dom 𝑈 ≠ ∅ |
20 | | dm0rn0 5834 |
. . . . . . . . . . . 12
⊢ (dom
𝑈 = ∅ ↔ ran
𝑈 =
∅) |
21 | 20 | necon3bii 2996 |
. . . . . . . . . . 11
⊢ (dom
𝑈 ≠ ∅ ↔ ran
𝑈 ≠
∅) |
22 | 19, 21 | mpbi 229 |
. . . . . . . . . 10
⊢ ran 𝑈 ≠ ∅ |
23 | | intssuni 4901 |
. . . . . . . . . 10
⊢ (ran
𝑈 ≠ ∅ → ∩ ran 𝑈 ⊆ ∪ ran
𝑈) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . 9
⊢ ∩ ran 𝑈 ⊆ ∪ ran
𝑈 |
25 | 3 | fin23lem16 10091 |
. . . . . . . . 9
⊢ ∪ ran 𝑈 = ∪ ran 𝑡 |
26 | 24, 25 | sseqtri 3957 |
. . . . . . . 8
⊢ ∩ ran 𝑈 ⊆ ∪ ran
𝑡 |
27 | 26 | sseli 3917 |
. . . . . . 7
⊢ (𝑎 ∈ ∩ ran 𝑈 → 𝑎 ∈ ∪ ran
𝑡) |
28 | | f1fun 6672 |
. . . . . . . . . . . . 13
⊢ (𝑡:ω–1-1→𝑉 → Fun 𝑡) |
29 | 28 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑡:ω–1-1→𝑉 ∧ ∪ ran
𝑡 ∈ 𝐹) → Fun 𝑡) |
30 | 3, 1, 4, 5, 6, 7 | fin23lem30 10098 |
. . . . . . . . . . . 12
⊢ (Fun
𝑡 → (∪ ran 𝑍 ∩ ∩ ran
𝑈) =
∅) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑡:ω–1-1→𝑉 ∧ ∪ ran
𝑡 ∈ 𝐹) → (∪ ran
𝑍 ∩ ∩ ran 𝑈) = ∅) |
32 | | disj 4381 |
. . . . . . . . . . 11
⊢ ((∪ ran 𝑍 ∩ ∩ ran
𝑈) = ∅ ↔
∀𝑎 ∈ ∪ ran 𝑍 ¬ 𝑎 ∈ ∩ ran
𝑈) |
33 | 31, 32 | sylib 217 |
. . . . . . . . . 10
⊢ ((𝑡:ω–1-1→𝑉 ∧ ∪ ran
𝑡 ∈ 𝐹) → ∀𝑎 ∈ ∪ ran
𝑍 ¬ 𝑎 ∈ ∩ ran
𝑈) |
34 | | rsp 3131 |
. . . . . . . . . 10
⊢
(∀𝑎 ∈
∪ ran 𝑍 ¬ 𝑎 ∈ ∩ ran
𝑈 → (𝑎 ∈ ∪ ran 𝑍 → ¬ 𝑎 ∈ ∩ ran
𝑈)) |
35 | 33, 34 | syl 17 |
. . . . . . . . 9
⊢ ((𝑡:ω–1-1→𝑉 ∧ ∪ ran
𝑡 ∈ 𝐹) → (𝑎 ∈ ∪ ran
𝑍 → ¬ 𝑎 ∈ ∩ ran 𝑈)) |
36 | 35 | con2d 134 |
. . . . . . . 8
⊢ ((𝑡:ω–1-1→𝑉 ∧ ∪ ran
𝑡 ∈ 𝐹) → (𝑎 ∈ ∩ ran
𝑈 → ¬ 𝑎 ∈ ∪ ran 𝑍)) |
37 | 36 | imp 407 |
. . . . . . 7
⊢ (((𝑡:ω–1-1→𝑉 ∧ ∪ ran
𝑡 ∈ 𝐹) ∧ 𝑎 ∈ ∩ ran
𝑈) → ¬ 𝑎 ∈ ∪ ran 𝑍) |
38 | | nelne1 3041 |
. . . . . . 7
⊢ ((𝑎 ∈ ∪ ran 𝑡 ∧ ¬ 𝑎 ∈ ∪ ran
𝑍) → ∪ ran 𝑡 ≠ ∪ ran 𝑍) |
39 | 27, 37, 38 | syl2an2 683 |
. . . . . 6
⊢ (((𝑡:ω–1-1→𝑉 ∧ ∪ ran
𝑡 ∈ 𝐹) ∧ 𝑎 ∈ ∩ ran
𝑈) → ∪ ran 𝑡 ≠ ∪ ran 𝑍) |
40 | 39 | necomd 2999 |
. . . . 5
⊢ (((𝑡:ω–1-1→𝑉 ∧ ∪ ran
𝑡 ∈ 𝐹) ∧ 𝑎 ∈ ∩ ran
𝑈) → ∪ ran 𝑍 ≠ ∪ ran 𝑡) |
41 | 13, 40 | exlimddv 1938 |
. . . 4
⊢ ((𝑡:ω–1-1→𝑉 ∧ ∪ ran
𝑡 ∈ 𝐹) → ∪ ran
𝑍 ≠ ∪ ran 𝑡) |
42 | | df-pss 3906 |
. . . 4
⊢ (∪ ran 𝑍 ⊊ ∪ ran
𝑡 ↔ (∪ ran 𝑍 ⊆ ∪ ran
𝑡 ∧ ∪ ran 𝑍 ≠ ∪ ran 𝑡)) |
43 | 9, 41, 42 | sylanbrc 583 |
. . 3
⊢ ((𝑡:ω–1-1→𝑉 ∧ ∪ ran
𝑡 ∈ 𝐹) → ∪ ran
𝑍 ⊊ ∪ ran 𝑡) |
44 | 2, 43 | sylan2 593 |
. 2
⊢ ((𝑡:ω–1-1→𝑉 ∧ (𝐺 ∈ 𝐹 ∧ ∪ ran
𝑡 ⊆ 𝐺)) → ∪ ran
𝑍 ⊊ ∪ ran 𝑡) |
45 | 44 | 3impb 1114 |
1
⊢ ((𝑡:ω–1-1→𝑉 ∧ 𝐺 ∈ 𝐹 ∧ ∪ ran
𝑡 ⊆ 𝐺) → ∪ ran
𝑍 ⊊ ∪ ran 𝑡) |