| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elex 3500 | . . . . 5
⊢ (suc
𝐴 ∈ Top → suc
𝐴 ∈
V) | 
| 2 |  | sucexb 7825 | . . . . 5
⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V) | 
| 3 | 1, 2 | sylibr 234 | . . . 4
⊢ (suc
𝐴 ∈ Top → 𝐴 ∈ V) | 
| 4 |  | sssucid 6463 | . . . . 5
⊢ 𝐴 ⊆ suc 𝐴 | 
| 5 |  | elpwg 4602 | . . . . 5
⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 suc 𝐴 ↔ 𝐴 ⊆ suc 𝐴)) | 
| 6 | 4, 5 | mpbiri 258 | . . . 4
⊢ (𝐴 ∈ V → 𝐴 ∈ 𝒫 suc 𝐴) | 
| 7 |  | limsucncmpi.1 | . . . . . . 7
⊢ Lim 𝐴 | 
| 8 |  | limuni 6444 | . . . . . . 7
⊢ (Lim
𝐴 → 𝐴 = ∪ 𝐴) | 
| 9 | 7, 8 | ax-mp 5 | . . . . . 6
⊢ 𝐴 = ∪
𝐴 | 
| 10 |  | elin 3966 | . . . . . . . . . 10
⊢ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑧 ∈ 𝒫 𝐴 ∧ 𝑧 ∈ Fin)) | 
| 11 |  | elpwi 4606 | . . . . . . . . . . 11
⊢ (𝑧 ∈ 𝒫 𝐴 → 𝑧 ⊆ 𝐴) | 
| 12 | 11 | anim1i 615 | . . . . . . . . . 10
⊢ ((𝑧 ∈ 𝒫 𝐴 ∧ 𝑧 ∈ Fin) → (𝑧 ⊆ 𝐴 ∧ 𝑧 ∈ Fin)) | 
| 13 | 10, 12 | sylbi 217 | . . . . . . . . 9
⊢ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) → (𝑧 ⊆ 𝐴 ∧ 𝑧 ∈ Fin)) | 
| 14 |  | nlim0 6442 | . . . . . . . . . . . . . . . 16
⊢  ¬
Lim ∅ | 
| 15 | 7, 14 | 2th 264 | . . . . . . . . . . . . . . 15
⊢ (Lim
𝐴 ↔ ¬ Lim
∅) | 
| 16 |  | xor3 382 | . . . . . . . . . . . . . . 15
⊢ (¬
(Lim 𝐴 ↔ Lim ∅)
↔ (Lim 𝐴 ↔ ¬
Lim ∅)) | 
| 17 | 15, 16 | mpbir 231 | . . . . . . . . . . . . . 14
⊢  ¬
(Lim 𝐴 ↔ Lim
∅) | 
| 18 |  | limeq 6395 | . . . . . . . . . . . . . . 15
⊢ (𝐴 = ∅ → (Lim 𝐴 ↔ Lim
∅)) | 
| 19 | 18 | necon3bi 2966 | . . . . . . . . . . . . . 14
⊢ (¬
(Lim 𝐴 ↔ Lim ∅)
→ 𝐴 ≠
∅) | 
| 20 | 17, 19 | ax-mp 5 | . . . . . . . . . . . . 13
⊢ 𝐴 ≠ ∅ | 
| 21 |  | uni0 4934 | . . . . . . . . . . . . 13
⊢ ∪ ∅ = ∅ | 
| 22 | 20, 21 | neeqtrri 3013 | . . . . . . . . . . . 12
⊢ 𝐴 ≠ ∪ ∅ | 
| 23 |  | unieq 4917 | . . . . . . . . . . . . 13
⊢ (𝑧 = ∅ → ∪ 𝑧 =
∪ ∅) | 
| 24 | 23 | neeq2d 3000 | . . . . . . . . . . . 12
⊢ (𝑧 = ∅ → (𝐴 ≠ ∪ 𝑧
↔ 𝐴 ≠ ∪ ∅)) | 
| 25 | 22, 24 | mpbiri 258 | . . . . . . . . . . 11
⊢ (𝑧 = ∅ → 𝐴 ≠ ∪ 𝑧) | 
| 26 | 25 | a1i 11 | . . . . . . . . . 10
⊢ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ∈ Fin) → (𝑧 = ∅ → 𝐴 ≠ ∪ 𝑧)) | 
| 27 |  | limord 6443 | . . . . . . . . . . . . . 14
⊢ (Lim
𝐴 → Ord 𝐴) | 
| 28 |  | ordsson 7804 | . . . . . . . . . . . . . 14
⊢ (Ord
𝐴 → 𝐴 ⊆ On) | 
| 29 | 7, 27, 28 | mp2b 10 | . . . . . . . . . . . . 13
⊢ 𝐴 ⊆ On | 
| 30 |  | sstr2 3989 | . . . . . . . . . . . . 13
⊢ (𝑧 ⊆ 𝐴 → (𝐴 ⊆ On → 𝑧 ⊆ On)) | 
| 31 | 29, 30 | mpi 20 | . . . . . . . . . . . 12
⊢ (𝑧 ⊆ 𝐴 → 𝑧 ⊆ On) | 
| 32 |  | ordunifi 9327 | . . . . . . . . . . . . 13
⊢ ((𝑧 ⊆ On ∧ 𝑧 ∈ Fin ∧ 𝑧 ≠ ∅) → ∪ 𝑧
∈ 𝑧) | 
| 33 | 32 | 3expia 1121 | . . . . . . . . . . . 12
⊢ ((𝑧 ⊆ On ∧ 𝑧 ∈ Fin) → (𝑧 ≠ ∅ → ∪ 𝑧
∈ 𝑧)) | 
| 34 | 31, 33 | sylan 580 | . . . . . . . . . . 11
⊢ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ∈ Fin) → (𝑧 ≠ ∅ → ∪ 𝑧
∈ 𝑧)) | 
| 35 |  | ssel 3976 | . . . . . . . . . . . . 13
⊢ (𝑧 ⊆ 𝐴 → (∪ 𝑧 ∈ 𝑧 → ∪ 𝑧 ∈ 𝐴)) | 
| 36 | 7, 27 | ax-mp 5 | . . . . . . . . . . . . . 14
⊢ Ord 𝐴 | 
| 37 |  | nordeq 6402 | . . . . . . . . . . . . . 14
⊢ ((Ord
𝐴 ∧ ∪ 𝑧
∈ 𝐴) → 𝐴 ≠ ∪ 𝑧) | 
| 38 | 36, 37 | mpan 690 | . . . . . . . . . . . . 13
⊢ (∪ 𝑧
∈ 𝐴 → 𝐴 ≠ ∪ 𝑧) | 
| 39 | 35, 38 | syl6 35 | . . . . . . . . . . . 12
⊢ (𝑧 ⊆ 𝐴 → (∪ 𝑧 ∈ 𝑧 → 𝐴 ≠ ∪ 𝑧)) | 
| 40 | 39 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ∈ Fin) → (∪ 𝑧
∈ 𝑧 → 𝐴 ≠ ∪ 𝑧)) | 
| 41 | 34, 40 | syld 47 | . . . . . . . . . 10
⊢ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ∈ Fin) → (𝑧 ≠ ∅ → 𝐴 ≠ ∪ 𝑧)) | 
| 42 | 26, 41 | pm2.61dne 3027 | . . . . . . . . 9
⊢ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ∈ Fin) → 𝐴 ≠ ∪ 𝑧) | 
| 43 | 13, 42 | syl 17 | . . . . . . . 8
⊢ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) → 𝐴 ≠ ∪ 𝑧) | 
| 44 | 43 | neneqd 2944 | . . . . . . 7
⊢ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) → ¬ 𝐴 = ∪
𝑧) | 
| 45 | 44 | nrex 3073 | . . . . . 6
⊢  ¬
∃𝑧 ∈ (𝒫
𝐴 ∩ Fin)𝐴 = ∪
𝑧 | 
| 46 |  | unieq 4917 | . . . . . . . . 9
⊢ (𝑦 = 𝐴 → ∪ 𝑦 = ∪
𝐴) | 
| 47 | 46 | eqeq2d 2747 | . . . . . . . 8
⊢ (𝑦 = 𝐴 → (𝐴 = ∪ 𝑦 ↔ 𝐴 = ∪ 𝐴)) | 
| 48 |  | pweq 4613 | . . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → 𝒫 𝑦 = 𝒫 𝐴) | 
| 49 | 48 | ineq1d 4218 | . . . . . . . . . 10
⊢ (𝑦 = 𝐴 → (𝒫 𝑦 ∩ Fin) = (𝒫 𝐴 ∩ Fin)) | 
| 50 | 49 | rexeqdv 3326 | . . . . . . . . 9
⊢ (𝑦 = 𝐴 → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝐴 = ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)𝐴 = ∪ 𝑧)) | 
| 51 | 50 | notbid 318 | . . . . . . . 8
⊢ (𝑦 = 𝐴 → (¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝐴 = ∪ 𝑧 ↔ ¬ ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)𝐴 = ∪ 𝑧)) | 
| 52 | 47, 51 | anbi12d 632 | . . . . . . 7
⊢ (𝑦 = 𝐴 → ((𝐴 = ∪ 𝑦 ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝐴 = ∪ 𝑧) ↔ (𝐴 = ∪ 𝐴 ∧ ¬ ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)𝐴 = ∪ 𝑧))) | 
| 53 | 52 | rspcev 3621 | . . . . . 6
⊢ ((𝐴 ∈ 𝒫 suc 𝐴 ∧ (𝐴 = ∪ 𝐴 ∧ ¬ ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)𝐴 = ∪ 𝑧)) → ∃𝑦 ∈ 𝒫 suc 𝐴(𝐴 = ∪ 𝑦 ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝐴 = ∪ 𝑧)) | 
| 54 | 9, 45, 53 | mpanr12 705 | . . . . 5
⊢ (𝐴 ∈ 𝒫 suc 𝐴 → ∃𝑦 ∈ 𝒫 suc 𝐴(𝐴 = ∪ 𝑦 ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝐴 = ∪ 𝑧)) | 
| 55 |  | rexanali 3101 | . . . . 5
⊢
(∃𝑦 ∈
𝒫 suc 𝐴(𝐴 = ∪
𝑦 ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝐴 = ∪ 𝑧) ↔ ¬ ∀𝑦 ∈ 𝒫 suc 𝐴(𝐴 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝐴 = ∪ 𝑧)) | 
| 56 | 54, 55 | sylib 218 | . . . 4
⊢ (𝐴 ∈ 𝒫 suc 𝐴 → ¬ ∀𝑦 ∈ 𝒫 suc 𝐴(𝐴 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝐴 = ∪ 𝑧)) | 
| 57 | 3, 6, 56 | 3syl 18 | . . 3
⊢ (suc
𝐴 ∈ Top → ¬
∀𝑦 ∈ 𝒫
suc 𝐴(𝐴 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝐴 = ∪ 𝑧)) | 
| 58 |  | imnan 399 | . . 3
⊢ ((suc
𝐴 ∈ Top → ¬
∀𝑦 ∈ 𝒫
suc 𝐴(𝐴 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝐴 = ∪ 𝑧)) ↔ ¬ (suc 𝐴 ∈ Top ∧ ∀𝑦 ∈ 𝒫 suc 𝐴(𝐴 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝐴 = ∪ 𝑧))) | 
| 59 | 57, 58 | mpbi 230 | . 2
⊢  ¬
(suc 𝐴 ∈ Top ∧
∀𝑦 ∈ 𝒫
suc 𝐴(𝐴 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝐴 = ∪ 𝑧)) | 
| 60 |  | ordunisuc 7853 | . . . . 5
⊢ (Ord
𝐴 → ∪ suc 𝐴 = 𝐴) | 
| 61 | 7, 27, 60 | mp2b 10 | . . . 4
⊢ ∪ suc 𝐴 = 𝐴 | 
| 62 | 61 | eqcomi 2745 | . . 3
⊢ 𝐴 = ∪
suc 𝐴 | 
| 63 | 62 | iscmp 23397 | . 2
⊢ (suc
𝐴 ∈ Comp ↔ (suc
𝐴 ∈ Top ∧
∀𝑦 ∈ 𝒫
suc 𝐴(𝐴 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝐴 = ∪ 𝑧))) | 
| 64 | 59, 63 | mtbir 323 | 1
⊢  ¬
suc 𝐴 ∈
Comp |