| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | limord 6443 | . . . . . . . . . 10
⊢ (Lim
𝐴 → Ord 𝐴) | 
| 2 |  | ordsson 7804 | . . . . . . . . . 10
⊢ (Ord
𝐴 → 𝐴 ⊆ On) | 
| 3 |  | sstr 3991 | . . . . . . . . . . 11
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ On) → 𝑥 ⊆ On) | 
| 4 | 3 | expcom 413 | . . . . . . . . . 10
⊢ (𝐴 ⊆ On → (𝑥 ⊆ 𝐴 → 𝑥 ⊆ On)) | 
| 5 | 1, 2, 4 | 3syl 18 | . . . . . . . . 9
⊢ (Lim
𝐴 → (𝑥 ⊆ 𝐴 → 𝑥 ⊆ On)) | 
| 6 |  | onsucuni 7849 | . . . . . . . . 9
⊢ (𝑥 ⊆ On → 𝑥 ⊆ suc ∪ 𝑥) | 
| 7 | 5, 6 | syl6 35 | . . . . . . . 8
⊢ (Lim
𝐴 → (𝑥 ⊆ 𝐴 → 𝑥 ⊆ suc ∪
𝑥)) | 
| 8 | 7 | adantrd 491 | . . . . . . 7
⊢ (Lim
𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴)) → 𝑥 ⊆ suc ∪
𝑥)) | 
| 9 | 8 | ralimdv 3168 | . . . . . 6
⊢ (Lim
𝐴 → (∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴)) → ∀𝑥 ∈ 𝐵 𝑥 ⊆ suc ∪
𝑥)) | 
| 10 |  | uniiun 5057 | . . . . . . 7
⊢ ∪ 𝐵 =
∪ 𝑥 ∈ 𝐵 𝑥 | 
| 11 |  | ss2iun 5009 | . . . . . . 7
⊢
(∀𝑥 ∈
𝐵 𝑥 ⊆ suc ∪
𝑥 → ∪ 𝑥 ∈ 𝐵 𝑥 ⊆ ∪
𝑥 ∈ 𝐵 suc ∪ 𝑥) | 
| 12 | 10, 11 | eqsstrid 4021 | . . . . . 6
⊢
(∀𝑥 ∈
𝐵 𝑥 ⊆ suc ∪
𝑥 → ∪ 𝐵
⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥) | 
| 13 | 9, 12 | syl6 35 | . . . . 5
⊢ (Lim
𝐴 → (∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴)) → ∪ 𝐵 ⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥)) | 
| 14 | 13 | imp 406 | . . . 4
⊢ ((Lim
𝐴 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴))) → ∪
𝐵 ⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥) | 
| 15 |  | cfslb.1 | . . . . . . . . . 10
⊢ 𝐴 ∈ V | 
| 16 | 15 | cfslbn 10308 | . . . . . . . . 9
⊢ ((Lim
𝐴 ∧ 𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴)) → ∪ 𝑥 ∈ 𝐴) | 
| 17 | 16 | 3expib 1122 | . . . . . . . 8
⊢ (Lim
𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴)) → ∪ 𝑥 ∈ 𝐴)) | 
| 18 |  | ordsucss 7839 | . . . . . . . 8
⊢ (Ord
𝐴 → (∪ 𝑥
∈ 𝐴 → suc ∪ 𝑥
⊆ 𝐴)) | 
| 19 | 1, 17, 18 | sylsyld 61 | . . . . . . 7
⊢ (Lim
𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴)) → suc ∪
𝑥 ⊆ 𝐴)) | 
| 20 | 19 | ralimdv 3168 | . . . . . 6
⊢ (Lim
𝐴 → (∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴)) → ∀𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴)) | 
| 21 |  | iunss 5044 | . . . . . 6
⊢ (∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴 ↔ ∀𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴) | 
| 22 | 20, 21 | imbitrrdi 252 | . . . . 5
⊢ (Lim
𝐴 → (∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴)) → ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴)) | 
| 23 | 22 | imp 406 | . . . 4
⊢ ((Lim
𝐴 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴))) → ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴) | 
| 24 |  | sseq1 4008 | . . . . . 6
⊢ (∪ 𝐵 =
𝐴 → (∪ 𝐵
⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ↔ 𝐴 ⊆ ∪
𝑥 ∈ 𝐵 suc ∪ 𝑥)) | 
| 25 |  | eqss 3998 | . . . . . . 7
⊢ (∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴 ↔ (∪
𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪
𝑥 ∈ 𝐵 suc ∪ 𝑥)) | 
| 26 | 25 | simplbi2com 502 | . . . . . 6
⊢ (𝐴 ⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 → (∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴 → ∪
𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴)) | 
| 27 | 24, 26 | biimtrdi 253 | . . . . 5
⊢ (∪ 𝐵 =
𝐴 → (∪ 𝐵
⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 → (∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴 → ∪
𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴))) | 
| 28 | 27 | com3l 89 | . . . 4
⊢ (∪ 𝐵
⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 → (∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴 → (∪ 𝐵 = 𝐴 → ∪
𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴))) | 
| 29 | 14, 23, 28 | sylc 65 | . . 3
⊢ ((Lim
𝐴 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴))) → (∪
𝐵 = 𝐴 → ∪
𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴)) | 
| 30 |  | limsuc 7871 | . . . . . . . . 9
⊢ (Lim
𝐴 → (∪ 𝑥
∈ 𝐴 ↔ suc ∪ 𝑥
∈ 𝐴)) | 
| 31 | 17, 30 | sylibd 239 | . . . . . . . 8
⊢ (Lim
𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴)) → suc ∪
𝑥 ∈ 𝐴)) | 
| 32 | 31 | ralimdv 3168 | . . . . . . 7
⊢ (Lim
𝐴 → (∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴)) → ∀𝑥 ∈ 𝐵 suc ∪ 𝑥 ∈ 𝐴)) | 
| 33 | 32 | imp 406 | . . . . . 6
⊢ ((Lim
𝐴 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴))) → ∀𝑥 ∈ 𝐵 suc ∪ 𝑥 ∈ 𝐴) | 
| 34 |  | r19.29 3113 | . . . . . . . 8
⊢
((∀𝑥 ∈
𝐵 suc ∪ 𝑥
∈ 𝐴 ∧ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥) → ∃𝑥 ∈ 𝐵 (suc ∪ 𝑥 ∈ 𝐴 ∧ 𝑦 = suc ∪ 𝑥)) | 
| 35 |  | eleq1 2828 | . . . . . . . . . 10
⊢ (𝑦 = suc ∪ 𝑥
→ (𝑦 ∈ 𝐴 ↔ suc ∪ 𝑥
∈ 𝐴)) | 
| 36 | 35 | biimparc 479 | . . . . . . . . 9
⊢ ((suc
∪ 𝑥 ∈ 𝐴 ∧ 𝑦 = suc ∪ 𝑥) → 𝑦 ∈ 𝐴) | 
| 37 | 36 | rexlimivw 3150 | . . . . . . . 8
⊢
(∃𝑥 ∈
𝐵 (suc ∪ 𝑥
∈ 𝐴 ∧ 𝑦 = suc ∪ 𝑥)
→ 𝑦 ∈ 𝐴) | 
| 38 | 34, 37 | syl 17 | . . . . . . 7
⊢
((∀𝑥 ∈
𝐵 suc ∪ 𝑥
∈ 𝐴 ∧ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥) → 𝑦 ∈ 𝐴) | 
| 39 | 38 | ex 412 | . . . . . 6
⊢
(∀𝑥 ∈
𝐵 suc ∪ 𝑥
∈ 𝐴 →
(∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 → 𝑦 ∈ 𝐴)) | 
| 40 | 33, 39 | syl 17 | . . . . 5
⊢ ((Lim
𝐴 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴))) → (∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 → 𝑦 ∈ 𝐴)) | 
| 41 | 40 | abssdv 4067 | . . . 4
⊢ ((Lim
𝐴 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴))) → {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} ⊆ 𝐴) | 
| 42 |  | vuniex 7760 | . . . . . . . 8
⊢ ∪ 𝑥
∈ V | 
| 43 | 42 | sucex 7827 | . . . . . . 7
⊢ suc ∪ 𝑥
∈ V | 
| 44 | 43 | dfiun2 5032 | . . . . . 6
⊢ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 = ∪
{𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} | 
| 45 | 44 | eqeq1i 2741 | . . . . 5
⊢ (∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴 ↔ ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} = 𝐴) | 
| 46 | 15 | cfslb 10307 | . . . . . 6
⊢ ((Lim
𝐴 ∧ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} ⊆ 𝐴 ∧ ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} = 𝐴) → (cf‘𝐴) ≼ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥}) | 
| 47 | 46 | 3expia 1121 | . . . . 5
⊢ ((Lim
𝐴 ∧ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} ⊆ 𝐴) → (∪
{𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} = 𝐴 → (cf‘𝐴) ≼ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥})) | 
| 48 | 45, 47 | biimtrid 242 | . . . 4
⊢ ((Lim
𝐴 ∧ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} ⊆ 𝐴) → (∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴 → (cf‘𝐴) ≼ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥})) | 
| 49 | 41, 48 | syldan 591 | . . 3
⊢ ((Lim
𝐴 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴))) → (∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴 → (cf‘𝐴) ≼ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥})) | 
| 50 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) = (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) | 
| 51 | 50 | rnmpt 5967 | . . . . . . . 8
⊢ ran
(𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} | 
| 52 | 43, 50 | fnmpti 6710 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) Fn 𝐵 | 
| 53 |  | dffn4 6825 | . . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) Fn 𝐵 ↔ (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥):𝐵–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥)) | 
| 54 | 52, 53 | mpbi 230 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥):𝐵–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) | 
| 55 |  | relsdom 8993 | . . . . . . . . . . 11
⊢ Rel
≺ | 
| 56 | 55 | brrelex1i 5740 | . . . . . . . . . 10
⊢ (𝐵 ≺ (cf‘𝐴) → 𝐵 ∈ V) | 
| 57 |  | breq1 5145 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝐵 → (𝑦 ≺ (cf‘𝐴) ↔ 𝐵 ≺ (cf‘𝐴))) | 
| 58 |  | foeq2 6816 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝐵 → ((𝑥 ∈ 𝐵 ↦ suc ∪
𝑥):𝑦–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) ↔ (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥):𝐵–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥))) | 
| 59 |  | breq2 5146 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝐵 → (ran (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) ≼ 𝑦 ↔ ran (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) ≼ 𝐵)) | 
| 60 | 58, 59 | imbi12d 344 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝐵 → (((𝑥 ∈ 𝐵 ↦ suc ∪
𝑥):𝑦–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) → ran (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) ≼ 𝑦) ↔ ((𝑥 ∈ 𝐵 ↦ suc ∪
𝑥):𝐵–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) → ran (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) ≼ 𝐵))) | 
| 61 | 57, 60 | imbi12d 344 | . . . . . . . . . . 11
⊢ (𝑦 = 𝐵 → ((𝑦 ≺ (cf‘𝐴) → ((𝑥 ∈ 𝐵 ↦ suc ∪
𝑥):𝑦–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) → ran (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) ≼ 𝑦)) ↔ (𝐵 ≺ (cf‘𝐴) → ((𝑥 ∈ 𝐵 ↦ suc ∪
𝑥):𝐵–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) → ran (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) ≼ 𝐵)))) | 
| 62 |  | cfon 10296 | . . . . . . . . . . . . 13
⊢
(cf‘𝐴) ∈
On | 
| 63 |  | sdomdom 9021 | . . . . . . . . . . . . 13
⊢ (𝑦 ≺ (cf‘𝐴) → 𝑦 ≼ (cf‘𝐴)) | 
| 64 |  | ondomen 10078 | . . . . . . . . . . . . 13
⊢
(((cf‘𝐴)
∈ On ∧ 𝑦 ≼
(cf‘𝐴)) → 𝑦 ∈ dom
card) | 
| 65 | 62, 63, 64 | sylancr 587 | . . . . . . . . . . . 12
⊢ (𝑦 ≺ (cf‘𝐴) → 𝑦 ∈ dom card) | 
| 66 |  | fodomnum 10098 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ dom card → ((𝑥 ∈ 𝐵 ↦ suc ∪
𝑥):𝑦–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) → ran (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) ≼ 𝑦)) | 
| 67 | 65, 66 | syl 17 | . . . . . . . . . . 11
⊢ (𝑦 ≺ (cf‘𝐴) → ((𝑥 ∈ 𝐵 ↦ suc ∪
𝑥):𝑦–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) → ran (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) ≼ 𝑦)) | 
| 68 | 61, 67 | vtoclg 3553 | . . . . . . . . . 10
⊢ (𝐵 ∈ V → (𝐵 ≺ (cf‘𝐴) → ((𝑥 ∈ 𝐵 ↦ suc ∪
𝑥):𝐵–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) → ran (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) ≼ 𝐵))) | 
| 69 | 56, 68 | mpcom 38 | . . . . . . . . 9
⊢ (𝐵 ≺ (cf‘𝐴) → ((𝑥 ∈ 𝐵 ↦ suc ∪
𝑥):𝐵–onto→ran (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) → ran (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) ≼ 𝐵)) | 
| 70 | 54, 69 | mpi 20 | . . . . . . . 8
⊢ (𝐵 ≺ (cf‘𝐴) → ran (𝑥 ∈ 𝐵 ↦ suc ∪
𝑥) ≼ 𝐵) | 
| 71 | 51, 70 | eqbrtrrid 5178 | . . . . . . 7
⊢ (𝐵 ≺ (cf‘𝐴) → {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} ≼ 𝐵) | 
| 72 |  | domtr 9048 | . . . . . . 7
⊢
(((cf‘𝐴)
≼ {𝑦 ∣
∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} ∧ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} ≼ 𝐵) → (cf‘𝐴) ≼ 𝐵) | 
| 73 | 71, 72 | sylan2 593 | . . . . . 6
⊢
(((cf‘𝐴)
≼ {𝑦 ∣
∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} ∧ 𝐵 ≺ (cf‘𝐴)) → (cf‘𝐴) ≼ 𝐵) | 
| 74 |  | domnsym 9140 | . . . . . 6
⊢
((cf‘𝐴)
≼ 𝐵 → ¬
𝐵 ≺ (cf‘𝐴)) | 
| 75 | 73, 74 | syl 17 | . . . . 5
⊢
(((cf‘𝐴)
≼ {𝑦 ∣
∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} ∧ 𝐵 ≺ (cf‘𝐴)) → ¬ 𝐵 ≺ (cf‘𝐴)) | 
| 76 | 75 | pm2.01da 798 | . . . 4
⊢
((cf‘𝐴)
≼ {𝑦 ∣
∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} → ¬ 𝐵 ≺ (cf‘𝐴)) | 
| 77 | 76 | a1i 11 | . . 3
⊢ ((Lim
𝐴 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴))) → ((cf‘𝐴) ≼ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥} → ¬ 𝐵 ≺ (cf‘𝐴))) | 
| 78 | 29, 49, 77 | 3syld 60 | . 2
⊢ ((Lim
𝐴 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴))) → (∪
𝐵 = 𝐴 → ¬ 𝐵 ≺ (cf‘𝐴))) | 
| 79 | 78 | necon2ad 2954 | 1
⊢ ((Lim
𝐴 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴))) → (𝐵 ≺ (cf‘𝐴) → ∪ 𝐵 ≠ 𝐴)) |