| Step | Hyp | Ref
| Expression |
| 1 | | simplrl 777 |
. . . . 5
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → 𝐵 ⊆ No
) |
| 2 | | simplrr 778 |
. . . . 5
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → 𝐵 ∈ V) |
| 3 | | simpll 767 |
. . . . . 6
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → 𝐴 ⊆ No
) |
| 4 | 3 | sselda 3983 |
. . . . 5
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ No
) |
| 5 | | noetainflem.1 |
. . . . . 6
⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {〈dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o〉}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) |
| 6 | 5 | noinfbnd2 27776 |
. . . . 5
⊢ ((𝐵 ⊆
No ∧ 𝐵 ∈ V
∧ 𝑎 ∈ No ) → (∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 ↔ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) |
| 7 | 1, 2, 4, 6 | syl3anc 1373 |
. . . 4
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → (∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 ↔ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) |
| 8 | | simplll 775 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝐴 ⊆ No
) |
| 9 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝑎 ∈ 𝐴) |
| 10 | 8, 9 | sseldd 3984 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝑎 ∈ No
) |
| 11 | | nodmord 27698 |
. . . . . . . . . 10
⊢ (𝑎 ∈
No → Ord dom 𝑎) |
| 12 | | ordirr 6402 |
. . . . . . . . . 10
⊢ (Ord dom
𝑎 → ¬ dom 𝑎 ∈ dom 𝑎) |
| 13 | 10, 11, 12 | 3syl 18 |
. . . . . . . . 9
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ¬ dom 𝑎 ∈ dom 𝑎) |
| 14 | | bdayval 27693 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈
No → ( bday ‘𝑎) = dom 𝑎) |
| 15 | 10, 14 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ( bday
‘𝑎) = dom
𝑎) |
| 16 | | bdayfo 27722 |
. . . . . . . . . . . . . . . 16
⊢ bday : No –onto→On |
| 17 | | fofn 6822 |
. . . . . . . . . . . . . . . 16
⊢ ( bday : No –onto→On → bday
Fn No ) |
| 18 | 16, 17 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ bday Fn No
|
| 19 | | fnfvima 7253 |
. . . . . . . . . . . . . . 15
⊢ (( bday Fn No ∧ 𝐴 ⊆
No ∧ 𝑎 ∈
𝐴) → ( bday ‘𝑎) ∈ ( bday
“ 𝐴)) |
| 20 | 18, 8, 9, 19 | mp3an2i 1468 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ( bday
‘𝑎) ∈
( bday “ 𝐴)) |
| 21 | 15, 20 | eqeltrrd 2842 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → dom 𝑎 ∈ ( bday
“ 𝐴)) |
| 22 | | elssuni 4937 |
. . . . . . . . . . . . 13
⊢ (dom
𝑎 ∈ ( bday “ 𝐴) → dom 𝑎 ⊆ ∪ ( bday “ 𝐴)) |
| 23 | 21, 22 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → dom 𝑎 ⊆ ∪ ( bday “ 𝐴)) |
| 24 | | nodmon 27695 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈
No → dom 𝑎
∈ On) |
| 25 | | imassrn 6089 |
. . . . . . . . . . . . . . . 16
⊢ ( bday “ 𝐴) ⊆ ran bday
|
| 26 | | forn 6823 |
. . . . . . . . . . . . . . . . 17
⊢ ( bday : No –onto→On → ran
bday = On) |
| 27 | 16, 26 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ ran bday = On |
| 28 | 25, 27 | sseqtri 4032 |
. . . . . . . . . . . . . . 15
⊢ ( bday “ 𝐴) ⊆ On |
| 29 | | ssorduni 7799 |
. . . . . . . . . . . . . . 15
⊢ (( bday “ 𝐴) ⊆ On → Ord ∪ ( bday “ 𝐴)) |
| 30 | 28, 29 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ Ord ∪ ( bday “ 𝐴) |
| 31 | | ordsssuc 6473 |
. . . . . . . . . . . . . 14
⊢ ((dom
𝑎 ∈ On ∧ Ord ∪ ( bday “ 𝐴)) → (dom 𝑎 ⊆ ∪ ( bday “ 𝐴) ↔ dom 𝑎 ∈ suc ∪
( bday “ 𝐴))) |
| 32 | 30, 31 | mpan2 691 |
. . . . . . . . . . . . 13
⊢ (dom
𝑎 ∈ On → (dom
𝑎 ⊆ ∪ ( bday “ 𝐴) ↔ dom 𝑎 ∈ suc ∪
( bday “ 𝐴))) |
| 33 | 10, 24, 32 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → (dom 𝑎 ⊆ ∪ ( bday “ 𝐴) ↔ dom 𝑎 ∈ suc ∪
( bday “ 𝐴))) |
| 34 | 23, 33 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → dom 𝑎 ∈ suc ∪
( bday “ 𝐴)) |
| 35 | | elun2 4183 |
. . . . . . . . . . 11
⊢ (dom
𝑎 ∈ suc ∪ ( bday “ 𝐴) → dom 𝑎 ∈ (dom 𝑇 ∪ suc ∪
( bday “ 𝐴))) |
| 36 | 34, 35 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → dom 𝑎 ∈ (dom 𝑇 ∪ suc ∪
( bday “ 𝐴))) |
| 37 | | eleq2 2830 |
. . . . . . . . . 10
⊢ (dom
𝑎 = (dom 𝑇 ∪ suc ∪
( bday “ 𝐴)) → (dom 𝑎 ∈ dom 𝑎 ↔ dom 𝑎 ∈ (dom 𝑇 ∪ suc ∪
( bday “ 𝐴)))) |
| 38 | 36, 37 | syl5ibrcom 247 |
. . . . . . . . 9
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → (dom 𝑎 = (dom 𝑇 ∪ suc ∪
( bday “ 𝐴)) → dom 𝑎 ∈ dom 𝑎)) |
| 39 | 13, 38 | mtod 198 |
. . . . . . . 8
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ¬ dom 𝑎 = (dom 𝑇 ∪ suc ∪
( bday “ 𝐴))) |
| 40 | | dmeq 5914 |
. . . . . . . . 9
⊢ (𝑎 = 𝑊 → dom 𝑎 = dom 𝑊) |
| 41 | | noetainflem.2 |
. . . . . . . . . . 11
⊢ 𝑊 = (𝑇 ∪ ((suc ∪
( bday “ 𝐴) ∖ dom 𝑇) × {2o})) |
| 42 | 41 | dmeqi 5915 |
. . . . . . . . . 10
⊢ dom 𝑊 = dom (𝑇 ∪ ((suc ∪
( bday “ 𝐴) ∖ dom 𝑇) × {2o})) |
| 43 | | dmun 5921 |
. . . . . . . . . 10
⊢ dom
(𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o})) = (dom 𝑇 ∪ dom ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o})) |
| 44 | | 2oex 8517 |
. . . . . . . . . . . . . 14
⊢
2o ∈ V |
| 45 | 44 | snnz 4776 |
. . . . . . . . . . . . 13
⊢
{2o} ≠ ∅ |
| 46 | | dmxp 5939 |
. . . . . . . . . . . . 13
⊢
({2o} ≠ ∅ → dom ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o}) = (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)) |
| 47 | 45, 46 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ dom ((suc
∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o}) = (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) |
| 48 | 47 | uneq2i 4165 |
. . . . . . . . . . 11
⊢ (dom
𝑇 ∪ dom ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o})) = (dom 𝑇 ∪ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)) |
| 49 | | undif2 4477 |
. . . . . . . . . . 11
⊢ (dom
𝑇 ∪ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)) = (dom 𝑇 ∪ suc ∪
( bday “ 𝐴)) |
| 50 | 48, 49 | eqtri 2765 |
. . . . . . . . . 10
⊢ (dom
𝑇 ∪ dom ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o})) = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴)) |
| 51 | 42, 43, 50 | 3eqtri 2769 |
. . . . . . . . 9
⊢ dom 𝑊 = (dom 𝑇 ∪ suc ∪
( bday “ 𝐴)) |
| 52 | 40, 51 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑎 = 𝑊 → dom 𝑎 = (dom 𝑇 ∪ suc ∪
( bday “ 𝐴))) |
| 53 | 39, 52 | nsyl 140 |
. . . . . . 7
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ¬ 𝑎 = 𝑊) |
| 54 | 53 | neqned 2947 |
. . . . . 6
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝑎 ≠ 𝑊) |
| 55 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) |
| 56 | 10 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑎 ∈ No
) |
| 57 | 56 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑎 ∈ No
) |
| 58 | | simp-4r 784 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝐴 ∈ V) |
| 59 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝐵 ⊆ No
) |
| 60 | 59 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝐵 ⊆ No
) |
| 61 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝐵 ∈ V) |
| 62 | 61 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝐵 ∈ V) |
| 63 | 5, 41 | noetainflem1 27782 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ V ∧ 𝐵 ⊆
No ∧ 𝐵 ∈
V) → 𝑊 ∈ No ) |
| 64 | 58, 60, 62, 63 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑊 ∈ No
) |
| 65 | 64 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑊 ∈ No
) |
| 66 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑎 ≠ 𝑊) |
| 67 | | nosepne 27725 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈
No ∧ 𝑊 ∈
No ∧ 𝑎 ≠ 𝑊) → (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})) |
| 68 | 57, 65, 66, 67 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})) |
| 69 | 55 | fvresd 6926 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑊 ↾ dom 𝑇)‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})) |
| 70 | | simp-4r 784 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝐵 ⊆ No
∧ 𝐵 ∈
V)) |
| 71 | 5, 41 | noetainflem2 27783 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ⊆
No ∧ 𝐵 ∈
V) → (𝑊 ↾ dom
𝑇) = 𝑇) |
| 72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑊 ↾ dom 𝑇) = 𝑇) |
| 73 | 72 | fveq1d 6908 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑊 ↾ dom 𝑇)‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})) |
| 74 | 69, 73 | eqtr3d 2779 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})) |
| 75 | 68, 74 | neeqtrd 3010 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})) |
| 76 | 75 | necomd 2996 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})) |
| 77 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 = ∩
{𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} → (𝑇‘𝑞) = (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})) |
| 78 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 = ∩
{𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} → (𝑎‘𝑞) = (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})) |
| 79 | 77, 78 | neeq12d 3002 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = ∩
{𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} → ((𝑇‘𝑞) ≠ (𝑎‘𝑞) ↔ (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))) |
| 80 | 79 | rspcev 3622 |
. . . . . . . . . . . . 13
⊢ ((∩ {𝑝
∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇 ∧ (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})) → ∃𝑞 ∈ dom 𝑇(𝑇‘𝑞) ≠ (𝑎‘𝑞)) |
| 81 | 55, 76, 80 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ∃𝑞 ∈ dom 𝑇(𝑇‘𝑞) ≠ (𝑎‘𝑞)) |
| 82 | | df-ne 2941 |
. . . . . . . . . . . . . . 15
⊢ ((𝑇‘𝑞) ≠ ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ ¬ (𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)) |
| 83 | | fvres 6925 |
. . . . . . . . . . . . . . . 16
⊢ (𝑞 ∈ dom 𝑇 → ((𝑎 ↾ dom 𝑇)‘𝑞) = (𝑎‘𝑞)) |
| 84 | 83 | neeq2d 3001 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 ∈ dom 𝑇 → ((𝑇‘𝑞) ≠ ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ (𝑇‘𝑞) ≠ (𝑎‘𝑞))) |
| 85 | 82, 84 | bitr3id 285 |
. . . . . . . . . . . . . 14
⊢ (𝑞 ∈ dom 𝑇 → (¬ (𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ (𝑇‘𝑞) ≠ (𝑎‘𝑞))) |
| 86 | 85 | rexbiia 3092 |
. . . . . . . . . . . . 13
⊢
(∃𝑞 ∈ dom
𝑇 ¬ (𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ ∃𝑞 ∈ dom 𝑇(𝑇‘𝑞) ≠ (𝑎‘𝑞)) |
| 87 | | rexnal 3100 |
. . . . . . . . . . . . 13
⊢
(∃𝑞 ∈ dom
𝑇 ¬ (𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)) |
| 88 | 86, 87 | bitr3i 277 |
. . . . . . . . . . . 12
⊢
(∃𝑞 ∈ dom
𝑇(𝑇‘𝑞) ≠ (𝑎‘𝑞) ↔ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)) |
| 89 | 81, 88 | sylib 218 |
. . . . . . . . . . 11
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)) |
| 90 | 89 | olcd 875 |
. . . . . . . . . 10
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))) |
| 91 | 5 | noinfno 27763 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ⊆
No ∧ 𝐵 ∈
V) → 𝑇 ∈ No ) |
| 92 | 91 | ad3antlr 731 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑇 ∈ No
) |
| 93 | 92 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑇 ∈ No
) |
| 94 | | nofun 27694 |
. . . . . . . . . . . . . 14
⊢ (𝑇 ∈
No → Fun 𝑇) |
| 95 | 93, 94 | syl 17 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → Fun 𝑇) |
| 96 | | nofun 27694 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈
No → Fun 𝑎) |
| 97 | | funres 6608 |
. . . . . . . . . . . . . 14
⊢ (Fun
𝑎 → Fun (𝑎 ↾ dom 𝑇)) |
| 98 | 57, 96, 97 | 3syl 18 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → Fun (𝑎 ↾ dom 𝑇)) |
| 99 | | eqfunfv 7056 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝑇 ∧ Fun (𝑎 ↾ dom 𝑇)) → (𝑇 = (𝑎 ↾ dom 𝑇) ↔ (dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∧ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)))) |
| 100 | 95, 98, 99 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇 = (𝑎 ↾ dom 𝑇) ↔ (dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∧ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)))) |
| 101 | | ianor 984 |
. . . . . . . . . . . . 13
⊢ (¬
(dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∧ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)) ↔ (¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))) |
| 102 | 101 | con1bii 356 |
. . . . . . . . . . . 12
⊢ (¬
(¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)) ↔ (dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∧ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))) |
| 103 | 100, 102 | bitr4di 289 |
. . . . . . . . . . 11
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇 = (𝑎 ↾ dom 𝑇) ↔ ¬ (¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)))) |
| 104 | 103 | con2bid 354 |
. . . . . . . . . 10
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)) ↔ ¬ 𝑇 = (𝑎 ↾ dom 𝑇))) |
| 105 | 90, 104 | mpbid 232 |
. . . . . . . . 9
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ¬ 𝑇 = (𝑎 ↾ dom 𝑇)) |
| 106 | 105 | pm2.21d 121 |
. . . . . . . 8
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇 = (𝑎 ↾ dom 𝑇) → 𝑎 <s 𝑊)) |
| 107 | 72 | breq2d 5155 |
. . . . . . . . 9
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑎 ↾ dom 𝑇) <s (𝑊 ↾ dom 𝑇) ↔ (𝑎 ↾ dom 𝑇) <s 𝑇)) |
| 108 | | nodmon 27695 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈
No → dom 𝑇
∈ On) |
| 109 | 92, 108 | syl 17 |
. . . . . . . . . . 11
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → dom 𝑇 ∈ On) |
| 110 | 109 | adantr 480 |
. . . . . . . . . 10
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → dom 𝑇 ∈ On) |
| 111 | | sltres 27707 |
. . . . . . . . . 10
⊢ ((𝑎 ∈
No ∧ 𝑊 ∈
No ∧ dom 𝑇 ∈ On) → ((𝑎 ↾ dom 𝑇) <s (𝑊 ↾ dom 𝑇) → 𝑎 <s 𝑊)) |
| 112 | 57, 65, 110, 111 | syl3anc 1373 |
. . . . . . . . 9
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑎 ↾ dom 𝑇) <s (𝑊 ↾ dom 𝑇) → 𝑎 <s 𝑊)) |
| 113 | 107, 112 | sylbird 260 |
. . . . . . . 8
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑎 ↾ dom 𝑇) <s 𝑇 → 𝑎 <s 𝑊)) |
| 114 | | simplrr 778 |
. . . . . . . . . 10
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → ¬ 𝑇 <s (𝑎 ↾ dom 𝑇)) |
| 115 | 114 | adantr 480 |
. . . . . . . . 9
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ¬ 𝑇 <s (𝑎 ↾ dom 𝑇)) |
| 116 | | noreson 27705 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈
No ∧ dom 𝑇
∈ On) → (𝑎
↾ dom 𝑇) ∈ No ) |
| 117 | 56, 109, 116 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → (𝑎 ↾ dom 𝑇) ∈ No
) |
| 118 | 117 | adantr 480 |
. . . . . . . . . . 11
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑎 ↾ dom 𝑇) ∈ No
) |
| 119 | | sltso 27721 |
. . . . . . . . . . . 12
⊢ <s Or
No |
| 120 | | sotric 5622 |
. . . . . . . . . . . 12
⊢ (( <s
Or No ∧ (𝑇 ∈ No
∧ (𝑎 ↾ dom 𝑇) ∈
No )) → (𝑇
<s (𝑎 ↾ dom 𝑇) ↔ ¬ (𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇))) |
| 121 | 119, 120 | mpan 690 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈
No ∧ (𝑎 ↾
dom 𝑇) ∈ No ) → (𝑇 <s (𝑎 ↾ dom 𝑇) ↔ ¬ (𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇))) |
| 122 | 93, 118, 121 | syl2anc 584 |
. . . . . . . . . 10
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇 <s (𝑎 ↾ dom 𝑇) ↔ ¬ (𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇))) |
| 123 | 122 | con2bid 354 |
. . . . . . . . 9
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇) ↔ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) |
| 124 | 115, 123 | mpbird 257 |
. . . . . . . 8
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇)) |
| 125 | 106, 113,
124 | mpjaod 861 |
. . . . . . 7
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑎 <s 𝑊) |
| 126 | 64 | adantr 480 |
. . . . . . . 8
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑊 ∈ No
) |
| 127 | 56 | adantr 480 |
. . . . . . . 8
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑎 ∈ No
) |
| 128 | | simplr 769 |
. . . . . . . . 9
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑎 ≠ 𝑊) |
| 129 | 128 | necomd 2996 |
. . . . . . . 8
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑊 ≠ 𝑎) |
| 130 | 41 | fveq1i 6907 |
. . . . . . . . 9
⊢ (𝑊‘∩ {𝑝
∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = ((𝑇 ∪ ((suc ∪
( bday “ 𝐴) ∖ dom 𝑇) × {2o}))‘∩ {𝑝
∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) |
| 131 | 92 | adantr 480 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑇 ∈ No
) |
| 132 | 131, 94 | syl 17 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → Fun 𝑇) |
| 133 | 132 | funfnd 6597 |
. . . . . . . . . . 11
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑇 Fn dom 𝑇) |
| 134 | | fnconstg 6796 |
. . . . . . . . . . . . 13
⊢
(2o ∈ V → ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o}) Fn (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)) |
| 135 | 44, 134 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((suc
∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o}) Fn (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) |
| 136 | 135 | a1i 11 |
. . . . . . . . . . 11
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ((suc ∪
( bday “ 𝐴) ∖ dom 𝑇) × {2o}) Fn (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)) |
| 137 | | disjdif 4472 |
. . . . . . . . . . . 12
⊢ (dom
𝑇 ∩ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)) = ∅ |
| 138 | 137 | a1i 11 |
. . . . . . . . . . 11
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → (dom 𝑇 ∩ (suc ∪
( bday “ 𝐴) ∖ dom 𝑇)) = ∅) |
| 139 | | nosepssdm 27731 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈
No ∧ 𝑊 ∈
No ∧ 𝑎 ≠ 𝑊) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ⊆ dom 𝑎) |
| 140 | 127, 126,
128, 139 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ∩
{𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ⊆ dom 𝑎) |
| 141 | 127, 14 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ( bday
‘𝑎) = dom
𝑎) |
| 142 | | simp-5l 785 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝐴 ⊆ No
) |
| 143 | | simplrl 777 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑎 ∈ 𝐴) |
| 144 | 143 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑎 ∈ 𝐴) |
| 145 | 18, 142, 144, 19 | mp3an2i 1468 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ( bday
‘𝑎) ∈
( bday “ 𝐴)) |
| 146 | | elssuni 4937 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑎) ∈ ( bday
“ 𝐴) → ( bday ‘𝑎) ⊆ ∪ ( bday “ 𝐴)) |
| 147 | 145, 146 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ( bday
‘𝑎) ⊆
∪ ( bday “ 𝐴)) |
| 148 | 141, 147 | eqsstrrd 4019 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → dom 𝑎 ⊆ ∪ ( bday “ 𝐴)) |
| 149 | 127, 24, 32 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → (dom 𝑎 ⊆ ∪ ( bday “ 𝐴) ↔ dom 𝑎 ∈ suc ∪
( bday “ 𝐴))) |
| 150 | 148, 149 | mpbid 232 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → dom 𝑎 ∈ suc ∪
( bday “ 𝐴)) |
| 151 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑎 ≠ 𝑊) |
| 152 | | nosepon 27710 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈
No ∧ 𝑊 ∈
No ∧ 𝑎 ≠ 𝑊) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On) |
| 153 | 56, 64, 151, 152 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On) |
| 154 | 153 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ∩
{𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On) |
| 155 | | eloni 6394 |
. . . . . . . . . . . . . 14
⊢ (∩ {𝑝
∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On → Ord ∩ {𝑝
∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) |
| 156 | | ordsuc 7833 |
. . . . . . . . . . . . . . . 16
⊢ (Ord
∪ ( bday “ 𝐴) ↔ Ord suc ∪ ( bday “ 𝐴)) |
| 157 | 30, 156 | mpbi 230 |
. . . . . . . . . . . . . . 15
⊢ Ord suc
∪ ( bday “ 𝐴) |
| 158 | | ordtr2 6428 |
. . . . . . . . . . . . . . 15
⊢ ((Ord
∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∧ Ord suc ∪
( bday “ 𝐴)) → ((∩
{𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ⊆ dom 𝑎 ∧ dom 𝑎 ∈ suc ∪
( bday “ 𝐴)) → ∩
{𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ suc ∪
( bday “ 𝐴))) |
| 159 | 157, 158 | mpan2 691 |
. . . . . . . . . . . . . 14
⊢ (Ord
∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} → ((∩
{𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ⊆ dom 𝑎 ∧ dom 𝑎 ∈ suc ∪
( bday “ 𝐴)) → ∩
{𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ suc ∪
( bday “ 𝐴))) |
| 160 | 154, 155,
159 | 3syl 18 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ((∩
{𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ⊆ dom 𝑎 ∧ dom 𝑎 ∈ suc ∪
( bday “ 𝐴)) → ∩
{𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ suc ∪
( bday “ 𝐴))) |
| 161 | 140, 150,
160 | mp2and 699 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ∩
{𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ suc ∪
( bday “ 𝐴)) |
| 162 | | ontri1 6418 |
. . . . . . . . . . . . . 14
⊢ ((dom
𝑇 ∈ On ∧ ∩ {𝑝
∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On) → (dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ↔ ¬ ∩
{𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇)) |
| 163 | 109, 153,
162 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → (dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ↔ ¬ ∩
{𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇)) |
| 164 | 163 | biimpa 476 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ¬ ∩
{𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) |
| 165 | 161, 164 | eldifd 3962 |
. . . . . . . . . . 11
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ∩
{𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ (suc ∪
( bday “ 𝐴) ∖ dom 𝑇)) |
| 166 | 133, 136,
138, 165 | fvun2d 7003 |
. . . . . . . . . 10
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ((𝑇 ∪ ((suc ∪
( bday “ 𝐴) ∖ dom 𝑇) × {2o}))‘∩ {𝑝
∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = (((suc ∪
( bday “ 𝐴) ∖ dom 𝑇) × {2o})‘∩ {𝑝
∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})) |
| 167 | 44 | fvconst2 7224 |
. . . . . . . . . . 11
⊢ (∩ {𝑝
∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ (suc ∪
( bday “ 𝐴) ∖ dom 𝑇) → (((suc ∪
( bday “ 𝐴) ∖ dom 𝑇) × {2o})‘∩ {𝑝
∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2o) |
| 168 | 165, 167 | syl 17 |
. . . . . . . . . 10
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → (((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o})‘∩ {𝑝
∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2o) |
| 169 | 166, 168 | eqtrd 2777 |
. . . . . . . . 9
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ((𝑇 ∪ ((suc ∪
( bday “ 𝐴) ∖ dom 𝑇) × {2o}))‘∩ {𝑝
∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2o) |
| 170 | 130, 169 | eqtrid 2789 |
. . . . . . . 8
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2o) |
| 171 | | nosep2o 27727 |
. . . . . . . 8
⊢ (((𝑊 ∈
No ∧ 𝑎 ∈
No ∧ 𝑊 ≠ 𝑎) ∧ (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2o) → 𝑎 <s 𝑊) |
| 172 | 126, 127,
129, 170, 171 | syl31anc 1375 |
. . . . . . 7
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑎 <s 𝑊) |
| 173 | 153, 155 | syl 17 |
. . . . . . . 8
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → Ord ∩
{𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) |
| 174 | | nodmord 27698 |
. . . . . . . . 9
⊢ (𝑇 ∈
No → Ord dom 𝑇) |
| 175 | 92, 174 | syl 17 |
. . . . . . . 8
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → Ord dom 𝑇) |
| 176 | | ordtri2or 6482 |
. . . . . . . 8
⊢ ((Ord
∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∧ Ord dom 𝑇) → (∩
{𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇 ∨ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})) |
| 177 | 173, 175,
176 | syl2anc 584 |
. . . . . . 7
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → (∩
{𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇 ∨ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})) |
| 178 | 125, 172,
177 | mpjaodan 961 |
. . . . . 6
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑎 <s 𝑊) |
| 179 | 54, 178 | mpdan 687 |
. . . . 5
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝑎 <s 𝑊) |
| 180 | 179 | expr 456 |
. . . 4
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → (¬ 𝑇 <s (𝑎 ↾ dom 𝑇) → 𝑎 <s 𝑊)) |
| 181 | 7, 180 | sylbid 240 |
. . 3
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → (∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 → 𝑎 <s 𝑊)) |
| 182 | 181 | ralimdva 3167 |
. 2
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 → ∀𝑎 ∈ 𝐴 𝑎 <s 𝑊)) |
| 183 | 182 | 3impia 1118 |
1
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ∀𝑎 ∈ 𝐴 𝑎 <s 𝑊) |