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