Proof of Theorem fin23lem31
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fin23lem17.f | . . . 4
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran
𝑎 ∈ ran 𝑎)} | 
| 2 | 1 | ssfin3ds 10370 | . . 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 10381 | . . . . 5
⊢ ∪ ran 𝑍 ⊆ ∪ ran
𝑡 | 
| 9 | 8 | a1i 11 | . . . 4
⊢ ((𝑡:ω–1-1→𝑉 ∧ ∪ ran
𝑡 ∈ 𝐹) → ∪ ran
𝑍 ⊆ ∪ ran 𝑡) | 
| 10 | 3, 1 | fin23lem21 10379 | . . . . . . 7
⊢ ((∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡:ω–1-1→𝑉) → ∩ ran
𝑈 ≠
∅) | 
| 11 | 10 | ancoms 458 | . . . . . 6
⊢ ((𝑡:ω–1-1→𝑉 ∧ ∪ ran
𝑡 ∈ 𝐹) → ∩ ran
𝑈 ≠
∅) | 
| 12 |  | n0 4353 | . . . . . 6
⊢ (∩ ran 𝑈 ≠ ∅ ↔ ∃𝑎 𝑎 ∈ ∩ ran
𝑈) | 
| 13 | 11, 12 | sylib 218 | . . . . 5
⊢ ((𝑡:ω–1-1→𝑉 ∧ ∪ ran
𝑡 ∈ 𝐹) → ∃𝑎 𝑎 ∈ ∩ ran
𝑈) | 
| 14 | 3 | fnseqom 8495 | . . . . . . . . . . . . 13
⊢ 𝑈 Fn ω | 
| 15 |  | fndm 6671 | . . . . . . . . . . . . 13
⊢ (𝑈 Fn ω → dom 𝑈 = ω) | 
| 16 | 14, 15 | ax-mp 5 | . . . . . . . . . . . 12
⊢ dom 𝑈 = ω | 
| 17 |  | peano1 7910 | . . . . . . . . . . . . 13
⊢ ∅
∈ ω | 
| 18 | 17 | ne0ii 4344 | . . . . . . . . . . . 12
⊢ ω
≠ ∅ | 
| 19 | 16, 18 | eqnetri 3011 | . . . . . . . . . . 11
⊢ dom 𝑈 ≠ ∅ | 
| 20 |  | dm0rn0 5935 | . . . . . . . . . . . 12
⊢ (dom
𝑈 = ∅ ↔ ran
𝑈 =
∅) | 
| 21 | 20 | necon3bii 2993 | . . . . . . . . . . 11
⊢ (dom
𝑈 ≠ ∅ ↔ ran
𝑈 ≠
∅) | 
| 22 | 19, 21 | mpbi 230 | . . . . . . . . . 10
⊢ ran 𝑈 ≠ ∅ | 
| 23 |  | intssuni 4970 | . . . . . . . . . 10
⊢ (ran
𝑈 ≠ ∅ → ∩ ran 𝑈 ⊆ ∪ ran
𝑈) | 
| 24 | 22, 23 | ax-mp 5 | . . . . . . . . 9
⊢ ∩ ran 𝑈 ⊆ ∪ ran
𝑈 | 
| 25 | 3 | fin23lem16 10375 | . . . . . . . . 9
⊢ ∪ ran 𝑈 = ∪ ran 𝑡 | 
| 26 | 24, 25 | sseqtri 4032 | . . . . . . . 8
⊢ ∩ ran 𝑈 ⊆ ∪ ran
𝑡 | 
| 27 | 26 | sseli 3979 | . . . . . . 7
⊢ (𝑎 ∈ ∩ ran 𝑈 → 𝑎 ∈ ∪ ran
𝑡) | 
| 28 |  | f1fun 6806 | . . . . . . . . . . . . 13
⊢ (𝑡:ω–1-1→𝑉 → Fun 𝑡) | 
| 29 | 28 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑡:ω–1-1→𝑉 ∧ ∪ ran
𝑡 ∈ 𝐹) → Fun 𝑡) | 
| 30 | 3, 1, 4, 5, 6, 7 | fin23lem30 10382 | . . . . . . . . . . . 12
⊢ (Fun
𝑡 → (∪ ran 𝑍 ∩ ∩ ran
𝑈) =
∅) | 
| 31 | 29, 30 | syl 17 | . . . . . . . . . . 11
⊢ ((𝑡:ω–1-1→𝑉 ∧ ∪ ran
𝑡 ∈ 𝐹) → (∪ ran
𝑍 ∩ ∩ ran 𝑈) = ∅) | 
| 32 |  | disj 4450 | . . . . . . . . . . 11
⊢ ((∪ ran 𝑍 ∩ ∩ ran
𝑈) = ∅ ↔
∀𝑎 ∈ ∪ ran 𝑍 ¬ 𝑎 ∈ ∩ ran
𝑈) | 
| 33 | 31, 32 | sylib 218 | . . . . . . . . . 10
⊢ ((𝑡:ω–1-1→𝑉 ∧ ∪ ran
𝑡 ∈ 𝐹) → ∀𝑎 ∈ ∪ ran
𝑍 ¬ 𝑎 ∈ ∩ ran
𝑈) | 
| 34 |  | rsp 3247 | . . . . . . . . . 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 406 | . . . . . . 7
⊢ (((𝑡:ω–1-1→𝑉 ∧ ∪ ran
𝑡 ∈ 𝐹) ∧ 𝑎 ∈ ∩ ran
𝑈) → ¬ 𝑎 ∈ ∪ ran 𝑍) | 
| 38 |  | nelne1 3039 | . . . . . . 7
⊢ ((𝑎 ∈ ∪ ran 𝑡 ∧ ¬ 𝑎 ∈ ∪ ran
𝑍) → ∪ ran 𝑡 ≠ ∪ ran 𝑍) | 
| 39 | 27, 37, 38 | syl2an2 686 | . . . . . 6
⊢ (((𝑡:ω–1-1→𝑉 ∧ ∪ ran
𝑡 ∈ 𝐹) ∧ 𝑎 ∈ ∩ ran
𝑈) → ∪ ran 𝑡 ≠ ∪ ran 𝑍) | 
| 40 | 39 | necomd 2996 | . . . . 5
⊢ (((𝑡:ω–1-1→𝑉 ∧ ∪ ran
𝑡 ∈ 𝐹) ∧ 𝑎 ∈ ∩ ran
𝑈) → ∪ ran 𝑍 ≠ ∪ ran 𝑡) | 
| 41 | 13, 40 | exlimddv 1935 | . . . 4
⊢ ((𝑡:ω–1-1→𝑉 ∧ ∪ ran
𝑡 ∈ 𝐹) → ∪ ran
𝑍 ≠ ∪ ran 𝑡) | 
| 42 |  | df-pss 3971 | . . . 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 1115 | 1
⊢ ((𝑡:ω–1-1→𝑉 ∧ 𝐺 ∈ 𝐹 ∧ ∪ ran
𝑡 ⊆ 𝐺) → ∪ ran
𝑍 ⊊ ∪ ran 𝑡) |