Proof of Theorem nosupinfsep
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ssun1 4178 | . . . . . . . 8
⊢ dom 𝑆 ⊆ (dom 𝑆 ∪ dom 𝑇) | 
| 2 |  | resabs1 6024 | . . . . . . . 8
⊢ (dom
𝑆 ⊆ (dom 𝑆 ∪ dom 𝑇) → ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑆) = (𝑊 ↾ dom 𝑆)) | 
| 3 | 1, 2 | ax-mp 5 | . . . . . . 7
⊢ ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑆) = (𝑊 ↾ dom 𝑆) | 
| 4 | 3 | breq1i 5150 | . . . . . 6
⊢ (((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑆) <s 𝑆 ↔ (𝑊 ↾ dom 𝑆) <s 𝑆) | 
| 5 | 4 | notbii 320 | . . . . 5
⊢ (¬
((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑆) <s 𝑆 ↔ ¬ (𝑊 ↾ dom 𝑆) <s 𝑆) | 
| 6 |  | ssun2 4179 | . . . . . . . 8
⊢ dom 𝑇 ⊆ (dom 𝑆 ∪ dom 𝑇) | 
| 7 |  | resabs1 6024 | . . . . . . . 8
⊢ (dom
𝑇 ⊆ (dom 𝑆 ∪ dom 𝑇) → ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑇) = (𝑊 ↾ dom 𝑇)) | 
| 8 | 6, 7 | ax-mp 5 | . . . . . . 7
⊢ ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑇) = (𝑊 ↾ dom 𝑇) | 
| 9 | 8 | breq2i 5151 | . . . . . 6
⊢ (𝑇 <s ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑇) ↔ 𝑇 <s (𝑊 ↾ dom 𝑇)) | 
| 10 | 9 | notbii 320 | . . . . 5
⊢ (¬
𝑇 <s ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑇) ↔ ¬ 𝑇 <s (𝑊 ↾ dom 𝑇)) | 
| 11 | 5, 10 | anbi12i 628 | . . . 4
⊢ ((¬
((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑆) <s 𝑆 ∧ ¬ 𝑇 <s ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑇)) ↔ (¬ (𝑊 ↾ dom 𝑆) <s 𝑆 ∧ ¬ 𝑇 <s (𝑊 ↾ dom 𝑇))) | 
| 12 | 11 | bicomi 224 | . . 3
⊢ ((¬
(𝑊 ↾ dom 𝑆) <s 𝑆 ∧ ¬ 𝑇 <s (𝑊 ↾ dom 𝑇)) ↔ (¬ ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑆) <s 𝑆 ∧ ¬ 𝑇 <s ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑇))) | 
| 13 | 12 | a1i 11 | . 2
⊢ (((𝐴 ⊆ 
No  ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆  No  ∧ 𝐵 ∈ V) ∧ 𝑊 ∈  No )
→ ((¬ (𝑊 ↾
dom 𝑆) <s 𝑆 ∧ ¬ 𝑇 <s (𝑊 ↾ dom 𝑇)) ↔ (¬ ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑆) <s 𝑆 ∧ ¬ 𝑇 <s ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑇)))) | 
| 14 |  | simp1l 1198 | . . . 4
⊢ (((𝐴 ⊆ 
No  ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆  No  ∧ 𝐵 ∈ V) ∧ 𝑊 ∈  No )
→ 𝐴 ⊆  No ) | 
| 15 |  | simp1r 1199 | . . . 4
⊢ (((𝐴 ⊆ 
No  ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆  No  ∧ 𝐵 ∈ V) ∧ 𝑊 ∈  No )
→ 𝐴 ∈
V) | 
| 16 |  | simp3 1139 | . . . 4
⊢ (((𝐴 ⊆ 
No  ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆  No  ∧ 𝐵 ∈ V) ∧ 𝑊 ∈  No )
→ 𝑊 ∈  No ) | 
| 17 |  | nosupinfsep.1 | . . . . 5
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) | 
| 18 | 17 | nosupbnd2 27761 | . . . 4
⊢ ((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑊 ∈  No ) → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑊 ↔ ¬ (𝑊 ↾ dom 𝑆) <s 𝑆)) | 
| 19 | 14, 15, 16, 18 | syl3anc 1373 | . . 3
⊢ (((𝐴 ⊆ 
No  ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆  No  ∧ 𝐵 ∈ V) ∧ 𝑊 ∈  No )
→ (∀𝑎 ∈
𝐴 𝑎 <s 𝑊 ↔ ¬ (𝑊 ↾ dom 𝑆) <s 𝑆)) | 
| 20 |  | simp2l 1200 | . . . 4
⊢ (((𝐴 ⊆ 
No  ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆  No  ∧ 𝐵 ∈ V) ∧ 𝑊 ∈  No )
→ 𝐵 ⊆  No ) | 
| 21 |  | simp2r 1201 | . . . 4
⊢ (((𝐴 ⊆ 
No  ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆  No  ∧ 𝐵 ∈ V) ∧ 𝑊 ∈  No )
→ 𝐵 ∈
V) | 
| 22 |  | nosupinfsep.2 | . . . . 5
⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {〈dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o〉}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) | 
| 23 | 22 | noinfbnd2 27776 | . . . 4
⊢ ((𝐵 ⊆ 
No  ∧ 𝐵 ∈ V
∧ 𝑊 ∈  No ) → (∀𝑏 ∈ 𝐵 𝑊 <s 𝑏 ↔ ¬ 𝑇 <s (𝑊 ↾ dom 𝑇))) | 
| 24 | 20, 21, 16, 23 | syl3anc 1373 | . . 3
⊢ (((𝐴 ⊆ 
No  ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆  No  ∧ 𝐵 ∈ V) ∧ 𝑊 ∈  No )
→ (∀𝑏 ∈
𝐵 𝑊 <s 𝑏 ↔ ¬ 𝑇 <s (𝑊 ↾ dom 𝑇))) | 
| 25 | 19, 24 | anbi12d 632 | . 2
⊢ (((𝐴 ⊆ 
No  ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆  No  ∧ 𝐵 ∈ V) ∧ 𝑊 ∈  No )
→ ((∀𝑎 ∈
𝐴 𝑎 <s 𝑊 ∧ ∀𝑏 ∈ 𝐵 𝑊 <s 𝑏) ↔ (¬ (𝑊 ↾ dom 𝑆) <s 𝑆 ∧ ¬ 𝑇 <s (𝑊 ↾ dom 𝑇)))) | 
| 26 | 17 | nosupno 27748 | . . . . . . . 8
⊢ ((𝐴 ⊆ 
No  ∧ 𝐴 ∈
V) → 𝑆 ∈  No ) | 
| 27 |  | nodmon 27695 | . . . . . . . 8
⊢ (𝑆 ∈ 
No  → dom 𝑆
∈ On) | 
| 28 | 26, 27 | syl 17 | . . . . . . 7
⊢ ((𝐴 ⊆ 
No  ∧ 𝐴 ∈
V) → dom 𝑆 ∈
On) | 
| 29 | 28 | 3ad2ant1 1134 | . . . . . 6
⊢ (((𝐴 ⊆ 
No  ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆  No  ∧ 𝐵 ∈ V) ∧ 𝑊 ∈  No )
→ dom 𝑆 ∈
On) | 
| 30 | 22 | noinfno 27763 | . . . . . . . 8
⊢ ((𝐵 ⊆ 
No  ∧ 𝐵 ∈
V) → 𝑇 ∈  No ) | 
| 31 |  | nodmon 27695 | . . . . . . . 8
⊢ (𝑇 ∈ 
No  → dom 𝑇
∈ On) | 
| 32 | 30, 31 | syl 17 | . . . . . . 7
⊢ ((𝐵 ⊆ 
No  ∧ 𝐵 ∈
V) → dom 𝑇 ∈
On) | 
| 33 | 32 | 3ad2ant2 1135 | . . . . . 6
⊢ (((𝐴 ⊆ 
No  ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆  No  ∧ 𝐵 ∈ V) ∧ 𝑊 ∈  No )
→ dom 𝑇 ∈
On) | 
| 34 |  | onun2 6492 | . . . . . 6
⊢ ((dom
𝑆 ∈ On ∧ dom 𝑇 ∈ On) → (dom 𝑆 ∪ dom 𝑇) ∈ On) | 
| 35 | 29, 33, 34 | syl2anc 584 | . . . . 5
⊢ (((𝐴 ⊆ 
No  ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆  No  ∧ 𝐵 ∈ V) ∧ 𝑊 ∈  No )
→ (dom 𝑆 ∪ dom
𝑇) ∈
On) | 
| 36 |  | noreson 27705 | . . . . 5
⊢ ((𝑊 ∈ 
No  ∧ (dom 𝑆
∪ dom 𝑇) ∈ On)
→ (𝑊 ↾ (dom
𝑆 ∪ dom 𝑇)) ∈ 
No ) | 
| 37 | 16, 35, 36 | syl2anc 584 | . . . 4
⊢ (((𝐴 ⊆ 
No  ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆  No  ∧ 𝐵 ∈ V) ∧ 𝑊 ∈  No )
→ (𝑊 ↾ (dom
𝑆 ∪ dom 𝑇)) ∈ 
No ) | 
| 38 | 17 | nosupbnd2 27761 | . . . 4
⊢ ((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ∈  No )
→ (∀𝑎 ∈
𝐴 𝑎 <s (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↔ ¬ ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑆) <s 𝑆)) | 
| 39 | 14, 15, 37, 38 | syl3anc 1373 | . . 3
⊢ (((𝐴 ⊆ 
No  ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆  No  ∧ 𝐵 ∈ V) ∧ 𝑊 ∈  No )
→ (∀𝑎 ∈
𝐴 𝑎 <s (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↔ ¬ ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑆) <s 𝑆)) | 
| 40 | 20, 21, 37 | 3jca 1129 | . . . 4
⊢ (((𝐴 ⊆ 
No  ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆  No  ∧ 𝐵 ∈ V) ∧ 𝑊 ∈  No )
→ (𝐵 ⊆  No  ∧ 𝐵 ∈ V ∧ (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ∈  No
)) | 
| 41 | 22 | noinfbnd2 27776 | . . . 4
⊢ ((𝐵 ⊆ 
No  ∧ 𝐵 ∈ V
∧ (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ∈  No )
→ (∀𝑏 ∈
𝐵 (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏 ↔ ¬ 𝑇 <s ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑇))) | 
| 42 | 40, 41 | syl 17 | . . 3
⊢ (((𝐴 ⊆ 
No  ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆  No  ∧ 𝐵 ∈ V) ∧ 𝑊 ∈  No )
→ (∀𝑏 ∈
𝐵 (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏 ↔ ¬ 𝑇 <s ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑇))) | 
| 43 | 39, 42 | anbi12d 632 | . 2
⊢ (((𝐴 ⊆ 
No  ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆  No  ∧ 𝐵 ∈ V) ∧ 𝑊 ∈  No )
→ ((∀𝑎 ∈
𝐴 𝑎 <s (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ∧ ∀𝑏 ∈ 𝐵 (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏) ↔ (¬ ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑆) <s 𝑆 ∧ ¬ 𝑇 <s ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑇)))) | 
| 44 | 13, 25, 43 | 3bitr4d 311 | 1
⊢ (((𝐴 ⊆ 
No  ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆  No  ∧ 𝐵 ∈ V) ∧ 𝑊 ∈  No )
→ ((∀𝑎 ∈
𝐴 𝑎 <s 𝑊 ∧ ∀𝑏 ∈ 𝐵 𝑊 <s 𝑏) ↔ (∀𝑎 ∈ 𝐴 𝑎 <s (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ∧ ∀𝑏 ∈ 𝐵 (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏))) |