| Step |
Hyp |
Ref |
Expression |
| 1 |
|
nosupbnd1.1 |
⊢ 𝑆 = if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) ) |
| 2 |
|
simpl1 |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) |
| 3 |
|
simpl2 |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ) |
| 4 |
|
simprl |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → 𝑤 ∈ 𝐴 ) |
| 5 |
|
simpl3 |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) |
| 6 |
|
simprr |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → 𝑈 <s 𝑤 ) |
| 7 |
|
simp2l |
⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → 𝐴 ⊆ No ) |
| 8 |
|
simp3l |
⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → 𝑈 ∈ 𝐴 ) |
| 9 |
7 8
|
sseldd |
⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → 𝑈 ∈ No ) |
| 10 |
|
simpl2l |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → 𝐴 ⊆ No ) |
| 11 |
10 4
|
sseldd |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → 𝑤 ∈ No ) |
| 12 |
|
ltsso |
⊢ <s Or No |
| 13 |
|
soasym |
⊢ ( ( <s Or No ∧ ( 𝑈 ∈ No ∧ 𝑤 ∈ No ) ) → ( 𝑈 <s 𝑤 → ¬ 𝑤 <s 𝑈 ) ) |
| 14 |
12 13
|
mpan |
⊢ ( ( 𝑈 ∈ No ∧ 𝑤 ∈ No ) → ( 𝑈 <s 𝑤 → ¬ 𝑤 <s 𝑈 ) ) |
| 15 |
9 11 14
|
syl2an2r |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑈 <s 𝑤 → ¬ 𝑤 <s 𝑈 ) ) |
| 16 |
6 15
|
mpd |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ¬ 𝑤 <s 𝑈 ) |
| 17 |
4 16
|
jca |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑤 ∈ 𝐴 ∧ ¬ 𝑤 <s 𝑈 ) ) |
| 18 |
1
|
nosupbnd1lem2 |
⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ∧ ( 𝑤 ∈ 𝐴 ∧ ¬ 𝑤 <s 𝑈 ) ) ) → ( 𝑤 ↾ dom 𝑆 ) = 𝑆 ) |
| 19 |
2 3 5 17 18
|
syl112anc |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑤 ↾ dom 𝑆 ) = 𝑆 ) |
| 20 |
1
|
nosupbnd1lem3 |
⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ 𝐴 ∧ ( 𝑤 ↾ dom 𝑆 ) = 𝑆 ) ) → ( 𝑤 ‘ dom 𝑆 ) ≠ 2o ) |
| 21 |
2 3 4 19 20
|
syl112anc |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑤 ‘ dom 𝑆 ) ≠ 2o ) |
| 22 |
21
|
neneqd |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ¬ ( 𝑤 ‘ dom 𝑆 ) = 2o ) |
| 23 |
22
|
expr |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ 𝑤 ∈ 𝐴 ) → ( 𝑈 <s 𝑤 → ¬ ( 𝑤 ‘ dom 𝑆 ) = 2o ) ) |
| 24 |
|
imnan |
⊢ ( ( 𝑈 <s 𝑤 → ¬ ( 𝑤 ‘ dom 𝑆 ) = 2o ) ↔ ¬ ( 𝑈 <s 𝑤 ∧ ( 𝑤 ‘ dom 𝑆 ) = 2o ) ) |
| 25 |
23 24
|
sylib |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ 𝑤 ∈ 𝐴 ) → ¬ ( 𝑈 <s 𝑤 ∧ ( 𝑤 ‘ dom 𝑆 ) = 2o ) ) |
| 26 |
25
|
nrexdv |
⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → ¬ ∃ 𝑤 ∈ 𝐴 ( 𝑈 <s 𝑤 ∧ ( 𝑤 ‘ dom 𝑆 ) = 2o ) ) |
| 27 |
|
simpl3l |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) → 𝑈 ∈ 𝐴 ) |
| 28 |
|
simpl1 |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) → ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) |
| 29 |
|
breq2 |
⊢ ( 𝑤 = 𝑦 → ( 𝑢 <s 𝑤 ↔ 𝑢 <s 𝑦 ) ) |
| 30 |
29
|
cbvrexvw |
⊢ ( ∃ 𝑤 ∈ 𝐴 𝑢 <s 𝑤 ↔ ∃ 𝑦 ∈ 𝐴 𝑢 <s 𝑦 ) |
| 31 |
|
breq1 |
⊢ ( 𝑢 = 𝑥 → ( 𝑢 <s 𝑦 ↔ 𝑥 <s 𝑦 ) ) |
| 32 |
31
|
rexbidv |
⊢ ( 𝑢 = 𝑥 → ( ∃ 𝑦 ∈ 𝐴 𝑢 <s 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 <s 𝑦 ) ) |
| 33 |
30 32
|
bitrid |
⊢ ( 𝑢 = 𝑥 → ( ∃ 𝑤 ∈ 𝐴 𝑢 <s 𝑤 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 <s 𝑦 ) ) |
| 34 |
33
|
cbvralvw |
⊢ ( ∀ 𝑢 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 𝑢 <s 𝑤 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 <s 𝑦 ) |
| 35 |
|
dfrex2 |
⊢ ( ∃ 𝑦 ∈ 𝐴 𝑥 <s 𝑦 ↔ ¬ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) |
| 36 |
35
|
ralbii |
⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 <s 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 ¬ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) |
| 37 |
|
ralnex |
⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ↔ ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) |
| 38 |
34 36 37
|
3bitri |
⊢ ( ∀ 𝑢 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 𝑢 <s 𝑤 ↔ ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) |
| 39 |
28 38
|
sylibr |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) → ∀ 𝑢 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 𝑢 <s 𝑤 ) |
| 40 |
|
breq1 |
⊢ ( 𝑢 = 𝑈 → ( 𝑢 <s 𝑤 ↔ 𝑈 <s 𝑤 ) ) |
| 41 |
40
|
rexbidv |
⊢ ( 𝑢 = 𝑈 → ( ∃ 𝑤 ∈ 𝐴 𝑢 <s 𝑤 ↔ ∃ 𝑤 ∈ 𝐴 𝑈 <s 𝑤 ) ) |
| 42 |
41
|
rspcv |
⊢ ( 𝑈 ∈ 𝐴 → ( ∀ 𝑢 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 𝑢 <s 𝑤 → ∃ 𝑤 ∈ 𝐴 𝑈 <s 𝑤 ) ) |
| 43 |
27 39 42
|
sylc |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) → ∃ 𝑤 ∈ 𝐴 𝑈 <s 𝑤 ) |
| 44 |
|
simpl2l |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) → 𝐴 ⊆ No ) |
| 45 |
44 27
|
sseldd |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) → 𝑈 ∈ No ) |
| 46 |
45
|
adantr |
⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → 𝑈 ∈ No ) |
| 47 |
44
|
adantr |
⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → 𝐴 ⊆ No ) |
| 48 |
|
simprl |
⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → 𝑤 ∈ 𝐴 ) |
| 49 |
47 48
|
sseldd |
⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → 𝑤 ∈ No ) |
| 50 |
1
|
nosupno |
⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) → 𝑆 ∈ No ) |
| 51 |
50
|
3ad2ant2 |
⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → 𝑆 ∈ No ) |
| 52 |
51
|
adantr |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) → 𝑆 ∈ No ) |
| 53 |
52
|
adantr |
⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → 𝑆 ∈ No ) |
| 54 |
|
nodmon |
⊢ ( 𝑆 ∈ No → dom 𝑆 ∈ On ) |
| 55 |
53 54
|
syl |
⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → dom 𝑆 ∈ On ) |
| 56 |
|
simpl3r |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) → ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) |
| 57 |
56
|
adantr |
⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) |
| 58 |
|
simpll1 |
⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) |
| 59 |
|
simpll2 |
⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ) |
| 60 |
|
simpll3 |
⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) |
| 61 |
|
simprr |
⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → 𝑈 <s 𝑤 ) |
| 62 |
45 49 14
|
syl2an2r |
⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑈 <s 𝑤 → ¬ 𝑤 <s 𝑈 ) ) |
| 63 |
61 62
|
mpd |
⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ¬ 𝑤 <s 𝑈 ) |
| 64 |
48 63
|
jca |
⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑤 ∈ 𝐴 ∧ ¬ 𝑤 <s 𝑈 ) ) |
| 65 |
58 59 60 64 18
|
syl112anc |
⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑤 ↾ dom 𝑆 ) = 𝑆 ) |
| 66 |
57 65
|
eqtr4d |
⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑈 ↾ dom 𝑆 ) = ( 𝑤 ↾ dom 𝑆 ) ) |
| 67 |
|
simplr |
⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑈 ‘ dom 𝑆 ) = ∅ ) |
| 68 |
|
nolt02o |
⊢ ( ( ( 𝑈 ∈ No ∧ 𝑤 ∈ No ∧ dom 𝑆 ∈ On ) ∧ ( ( 𝑈 ↾ dom 𝑆 ) = ( 𝑤 ↾ dom 𝑆 ) ∧ 𝑈 <s 𝑤 ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) → ( 𝑤 ‘ dom 𝑆 ) = 2o ) |
| 69 |
46 49 55 66 61 67 68
|
syl321anc |
⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑤 ‘ dom 𝑆 ) = 2o ) |
| 70 |
69
|
expr |
⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ 𝑤 ∈ 𝐴 ) → ( 𝑈 <s 𝑤 → ( 𝑤 ‘ dom 𝑆 ) = 2o ) ) |
| 71 |
70
|
ancld |
⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ 𝑤 ∈ 𝐴 ) → ( 𝑈 <s 𝑤 → ( 𝑈 <s 𝑤 ∧ ( 𝑤 ‘ dom 𝑆 ) = 2o ) ) ) |
| 72 |
71
|
reximdva |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) → ( ∃ 𝑤 ∈ 𝐴 𝑈 <s 𝑤 → ∃ 𝑤 ∈ 𝐴 ( 𝑈 <s 𝑤 ∧ ( 𝑤 ‘ dom 𝑆 ) = 2o ) ) ) |
| 73 |
43 72
|
mpd |
⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) → ∃ 𝑤 ∈ 𝐴 ( 𝑈 <s 𝑤 ∧ ( 𝑤 ‘ dom 𝑆 ) = 2o ) ) |
| 74 |
26 73
|
mtand |
⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → ¬ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) |
| 75 |
74
|
neqned |
⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → ( 𝑈 ‘ dom 𝑆 ) ≠ ∅ ) |