| Step | Hyp | Ref
| Expression |
| 1 | | ralcom 3289 |
. . 3
⊢
(∀𝑎 ∈
𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 ↔ ∀𝑏 ∈ 𝐵 ∀𝑎 ∈ 𝐴 𝑎 <s 𝑏) |
| 2 | | simplll 775 |
. . . . . 6
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → 𝐴 ⊆ No
) |
| 3 | | simpllr 776 |
. . . . . 6
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → 𝐴 ∈ V) |
| 4 | | simprl 771 |
. . . . . . 7
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → 𝐵 ⊆ No
) |
| 5 | 4 | sselda 3983 |
. . . . . 6
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ No
) |
| 6 | | noetasuplem.1 |
. . . . . . 7
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) |
| 7 | 6 | nosupbnd2 27761 |
. . . . . 6
⊢ ((𝐴 ⊆
No ∧ 𝐴 ∈ V
∧ 𝑏 ∈ No ) → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑏 ↔ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) |
| 8 | 2, 3, 5, 7 | syl3anc 1373 |
. . . . 5
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑏 ↔ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) |
| 9 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆) → 𝑏 ∈ 𝐵) |
| 10 | | ssel2 3978 |
. . . . . . . . . . 11
⊢ ((𝐵 ⊆
No ∧ 𝑏 ∈
𝐵) → 𝑏 ∈
No ) |
| 11 | 4, 9, 10 | syl2an 596 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝑏 ∈ No
) |
| 12 | | nodmord 27698 |
. . . . . . . . . 10
⊢ (𝑏 ∈
No → Ord dom 𝑏) |
| 13 | | ordirr 6402 |
. . . . . . . . . 10
⊢ (Ord dom
𝑏 → ¬ dom 𝑏 ∈ dom 𝑏) |
| 14 | 11, 12, 13 | 3syl 18 |
. . . . . . . . 9
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ¬ dom 𝑏 ∈ dom 𝑏) |
| 15 | | ssun2 4179 |
. . . . . . . . . . 11
⊢ suc ∪ ( bday “ 𝐵) ⊆ (dom 𝑆 ∪ suc ∪
( bday “ 𝐵)) |
| 16 | | bdayval 27693 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈
No → ( bday ‘𝑏) = dom 𝑏) |
| 17 | 11, 16 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ( bday
‘𝑏) = dom
𝑏) |
| 18 | | bdayfo 27722 |
. . . . . . . . . . . . . . . . 17
⊢ bday : No –onto→On |
| 19 | | fofn 6822 |
. . . . . . . . . . . . . . . . 17
⊢ ( bday : No –onto→On → bday
Fn No ) |
| 20 | 18, 19 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ bday Fn No
|
| 21 | | fnfvima 7253 |
. . . . . . . . . . . . . . . 16
⊢ (( bday Fn No ∧ 𝐵 ⊆
No ∧ 𝑏 ∈
𝐵) → ( bday ‘𝑏) ∈ ( bday
“ 𝐵)) |
| 22 | 20, 21 | mp3an1 1450 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ⊆
No ∧ 𝑏 ∈
𝐵) → ( bday ‘𝑏) ∈ ( bday
“ 𝐵)) |
| 23 | 4, 9, 22 | syl2an 596 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ( bday
‘𝑏) ∈
( bday “ 𝐵)) |
| 24 | 17, 23 | eqeltrrd 2842 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ∈ ( bday
“ 𝐵)) |
| 25 | | elssuni 4937 |
. . . . . . . . . . . . 13
⊢ (dom
𝑏 ∈ ( bday “ 𝐵) → dom 𝑏 ⊆ ∪ ( bday “ 𝐵)) |
| 26 | 24, 25 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ⊆ ∪ ( bday “ 𝐵)) |
| 27 | | nodmon 27695 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈
No → dom 𝑏
∈ On) |
| 28 | | imassrn 6089 |
. . . . . . . . . . . . . . . 16
⊢ ( bday “ 𝐵) ⊆ ran bday
|
| 29 | | forn 6823 |
. . . . . . . . . . . . . . . . 17
⊢ ( bday : No –onto→On → ran
bday = On) |
| 30 | 18, 29 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ ran bday = On |
| 31 | 28, 30 | sseqtri 4032 |
. . . . . . . . . . . . . . 15
⊢ ( bday “ 𝐵) ⊆ On |
| 32 | | ssorduni 7799 |
. . . . . . . . . . . . . . 15
⊢ (( bday “ 𝐵) ⊆ On → Ord ∪ ( bday “ 𝐵)) |
| 33 | 31, 32 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ Ord ∪ ( bday “ 𝐵) |
| 34 | | ordsssuc 6473 |
. . . . . . . . . . . . . 14
⊢ ((dom
𝑏 ∈ On ∧ Ord ∪ ( bday “ 𝐵)) → (dom 𝑏 ⊆ ∪ ( bday “ 𝐵) ↔ dom 𝑏 ∈ suc ∪
( bday “ 𝐵))) |
| 35 | 33, 34 | mpan2 691 |
. . . . . . . . . . . . 13
⊢ (dom
𝑏 ∈ On → (dom
𝑏 ⊆ ∪ ( bday “ 𝐵) ↔ dom 𝑏 ∈ suc ∪
( bday “ 𝐵))) |
| 36 | 11, 27, 35 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → (dom 𝑏 ⊆ ∪ ( bday “ 𝐵) ↔ dom 𝑏 ∈ suc ∪
( bday “ 𝐵))) |
| 37 | 26, 36 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ∈ suc ∪
( bday “ 𝐵)) |
| 38 | 15, 37 | sselid 3981 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ∈ (dom 𝑆 ∪ suc ∪
( bday “ 𝐵))) |
| 39 | | eleq2 2830 |
. . . . . . . . . 10
⊢ ((dom
𝑆 ∪ suc ∪ ( bday “ 𝐵)) = dom 𝑏 → (dom 𝑏 ∈ (dom 𝑆 ∪ suc ∪
( bday “ 𝐵)) ↔ dom 𝑏 ∈ dom 𝑏)) |
| 40 | 38, 39 | syl5ibcom 245 |
. . . . . . . . 9
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ((dom 𝑆 ∪ suc ∪
( bday “ 𝐵)) = dom 𝑏 → dom 𝑏 ∈ dom 𝑏)) |
| 41 | 14, 40 | mtod 198 |
. . . . . . . 8
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ¬ (dom 𝑆 ∪ suc ∪
( bday “ 𝐵)) = dom 𝑏) |
| 42 | | noetasuplem.2 |
. . . . . . . . . . . 12
⊢ 𝑍 = (𝑆 ∪ ((suc ∪
( bday “ 𝐵) ∖ dom 𝑆) × {1o})) |
| 43 | 42 | dmeqi 5915 |
. . . . . . . . . . 11
⊢ dom 𝑍 = dom (𝑆 ∪ ((suc ∪
( bday “ 𝐵) ∖ dom 𝑆) × {1o})) |
| 44 | | dmun 5921 |
. . . . . . . . . . 11
⊢ dom
(𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o})) = (dom 𝑆 ∪ dom ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o})) |
| 45 | 43, 44 | eqtri 2765 |
. . . . . . . . . 10
⊢ dom 𝑍 = (dom 𝑆 ∪ dom ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o})) |
| 46 | | 1oex 8516 |
. . . . . . . . . . . . 13
⊢
1o ∈ V |
| 47 | 46 | snnz 4776 |
. . . . . . . . . . . 12
⊢
{1o} ≠ ∅ |
| 48 | | dmxp 5939 |
. . . . . . . . . . . 12
⊢
({1o} ≠ ∅ → dom ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}) = (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)) |
| 49 | 47, 48 | ax-mp 5 |
. . . . . . . . . . 11
⊢ dom ((suc
∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}) = (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) |
| 50 | 49 | uneq2i 4165 |
. . . . . . . . . 10
⊢ (dom
𝑆 ∪ dom ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o})) = (dom 𝑆 ∪ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)) |
| 51 | | undif2 4477 |
. . . . . . . . . 10
⊢ (dom
𝑆 ∪ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)) = (dom 𝑆 ∪ suc ∪
( bday “ 𝐵)) |
| 52 | 45, 50, 51 | 3eqtri 2769 |
. . . . . . . . 9
⊢ dom 𝑍 = (dom 𝑆 ∪ suc ∪
( bday “ 𝐵)) |
| 53 | | dmeq 5914 |
. . . . . . . . 9
⊢ (𝑍 = 𝑏 → dom 𝑍 = dom 𝑏) |
| 54 | 52, 53 | eqtr3id 2791 |
. . . . . . . 8
⊢ (𝑍 = 𝑏 → (dom 𝑆 ∪ suc ∪
( bday “ 𝐵)) = dom 𝑏) |
| 55 | 41, 54 | nsyl 140 |
. . . . . . 7
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ¬ 𝑍 = 𝑏) |
| 56 | | df-ne 2941 |
. . . . . . . 8
⊢ (𝑍 ≠ 𝑏 ↔ ¬ 𝑍 = 𝑏) |
| 57 | | notnotr 130 |
. . . . . . . . . . . . . . 15
⊢ (¬
¬ dom (𝑏 ↾ dom
𝑆) = dom 𝑆 → dom (𝑏 ↾ dom 𝑆) = dom 𝑆) |
| 58 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) |
| 59 | 58 | fvresd 6926 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})) |
| 60 | 42 | reseq1i 5993 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑍 ↾ dom 𝑆) = ((𝑆 ∪ ((suc ∪
( bday “ 𝐵) ∖ dom 𝑆) × {1o})) ↾ dom
𝑆) |
| 61 | | resundir 6012 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o})) ↾ dom
𝑆) = ((𝑆 ↾ dom 𝑆) ∪ (((suc ∪
( bday “ 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆)) |
| 62 | | df-res 5697 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((suc
∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆) = (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}) ∩ (dom 𝑆 × V)) |
| 63 | | disjdifr 4473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((suc
∪ ( bday “ 𝐵) ∖ dom 𝑆) ∩ dom 𝑆) = ∅ |
| 64 | | xpdisj1 6181 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((suc
∪ ( bday “ 𝐵) ∖ dom 𝑆) ∩ dom 𝑆) = ∅ → (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}) ∩ (dom 𝑆 × V)) =
∅) |
| 65 | 63, 64 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((suc
∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}) ∩ (dom 𝑆 × V)) =
∅ |
| 66 | 62, 65 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((suc
∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆) = ∅ |
| 67 | 66 | uneq2i 4165 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑆 ↾ dom 𝑆) ∪ (((suc ∪
( bday “ 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆)) = ((𝑆 ↾ dom 𝑆) ∪ ∅) |
| 68 | | un0 4394 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑆 ↾ dom 𝑆) ∪ ∅) = (𝑆 ↾ dom 𝑆) |
| 69 | 67, 68 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑆 ↾ dom 𝑆) ∪ (((suc ∪
( bday “ 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆)) = (𝑆 ↾ dom 𝑆) |
| 70 | 60, 61, 69 | 3eqtri 2769 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑍 ↾ dom 𝑆) = (𝑆 ↾ dom 𝑆) |
| 71 | | simplll 775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → (𝐴 ⊆ No
∧ 𝐴 ∈
V)) |
| 72 | 6 | nosupno 27748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ⊆
No ∧ 𝐴 ∈
V) → 𝑆 ∈ No ) |
| 73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝑆 ∈ No
) |
| 74 | 73 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → 𝑆 ∈ No
) |
| 75 | | nofun 27694 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑆 ∈
No → Fun 𝑆) |
| 76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → Fun 𝑆) |
| 77 | | funrel 6583 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (Fun
𝑆 → Rel 𝑆) |
| 78 | | resdm 6044 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (Rel
𝑆 → (𝑆 ↾ dom 𝑆) = 𝑆) |
| 79 | 76, 77, 78 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑆 ↾ dom 𝑆) = 𝑆) |
| 80 | 70, 79 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑍 ↾ dom 𝑆) = 𝑆) |
| 81 | 80 | fveq1d 6908 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})) |
| 82 | 59, 81 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})) |
| 83 | | simp-4l 783 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝐴 ⊆ No
) |
| 84 | | simp-4r 784 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝐴 ∈ V) |
| 85 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝐵 ∈ V) |
| 86 | 85 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝐵 ∈ V) |
| 87 | 6, 42 | noetasuplem1 27778 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ⊆
No ∧ 𝐴 ∈ V
∧ 𝐵 ∈ V) →
𝑍 ∈ No ) |
| 88 | 83, 84, 86, 87 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝑍 ∈ No
) |
| 89 | 88 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → 𝑍 ∈ No
) |
| 90 | 11 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝑏 ∈ No
) |
| 91 | 90 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → 𝑏 ∈ No
) |
| 92 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → 𝑍 ≠ 𝑏) |
| 93 | | nosepne 27725 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑍 ∈
No ∧ 𝑏 ∈
No ∧ 𝑍 ≠ 𝑏) → (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ (𝑏‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})) |
| 94 | 89, 91, 92, 93 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ (𝑏‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})) |
| 95 | 82, 94 | eqnetrrd 3009 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ (𝑏‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})) |
| 96 | 58 | fvresd 6926 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (𝑏‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})) |
| 97 | 95, 96 | neeqtrrd 3015 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})) |
| 98 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑞 = ∩
{𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} → ((𝑏 ↾ dom 𝑆)‘𝑞) = ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})) |
| 99 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑞 = ∩
{𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} → (𝑆‘𝑞) = (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})) |
| 100 | 98, 99 | neeq12d 3002 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑞 = ∩
{𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} → (((𝑏 ↾ dom 𝑆)‘𝑞) ≠ (𝑆‘𝑞) ↔ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))) |
| 101 | | df-ne 2941 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑏 ↾ dom 𝑆)‘𝑞) ≠ (𝑆‘𝑞) ↔ ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)) |
| 102 | | necom 2994 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ↔ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})) |
| 103 | 100, 101,
102 | 3bitr3g 313 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑞 = ∩
{𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} → (¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞) ↔ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))) |
| 104 | 103 | rspcev 3622 |
. . . . . . . . . . . . . . . . . 18
⊢ ((∩ {𝑝
∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆 ∧ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})) → ∃𝑞 ∈ dom 𝑆 ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)) |
| 105 | 58, 97, 104 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ∃𝑞 ∈ dom 𝑆 ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)) |
| 106 | | rexeq 3322 |
. . . . . . . . . . . . . . . . 17
⊢ (dom
(𝑏 ↾ dom 𝑆) = dom 𝑆 → (∃𝑞 ∈ dom (𝑏 ↾ dom 𝑆) ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞) ↔ ∃𝑞 ∈ dom 𝑆 ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))) |
| 107 | 105, 106 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → ∃𝑞 ∈ dom (𝑏 ↾ dom 𝑆) ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))) |
| 108 | | rexnal 3100 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑞 ∈ dom
(𝑏 ↾ dom 𝑆) ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞) ↔ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)) |
| 109 | 107, 108 | imbitrdi 251 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))) |
| 110 | 57, 109 | syl5 34 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (¬ ¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))) |
| 111 | 110 | orrd 864 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))) |
| 112 | | nofun 27694 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈
No → Fun 𝑏) |
| 113 | | funres 6608 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
𝑏 → Fun (𝑏 ↾ dom 𝑆)) |
| 114 | 91, 112, 113 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → Fun (𝑏 ↾ dom 𝑆)) |
| 115 | | eqfunfv 7056 |
. . . . . . . . . . . . . . . 16
⊢ ((Fun
(𝑏 ↾ dom 𝑆) ∧ Fun 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 ↔ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)))) |
| 116 | 114, 76, 115 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 ↔ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)))) |
| 117 | | ianor 984 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)) ↔ (¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))) |
| 118 | 117 | con1bii 356 |
. . . . . . . . . . . . . . 15
⊢ (¬
(¬ dom (𝑏 ↾ dom
𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)) ↔ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))) |
| 119 | 116, 118 | bitr4di 289 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 ↔ ¬ (¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)))) |
| 120 | 119 | con2bid 354 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)) ↔ ¬ (𝑏 ↾ dom 𝑆) = 𝑆)) |
| 121 | 111, 120 | mpbid 232 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ¬ (𝑏 ↾ dom 𝑆) = 𝑆) |
| 122 | 121 | pm2.21d 121 |
. . . . . . . . . . 11
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 → 𝑍 <s 𝑏)) |
| 123 | 80 | breq1d 5153 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆) <s (𝑏 ↾ dom 𝑆) ↔ 𝑆 <s (𝑏 ↾ dom 𝑆))) |
| 124 | | nodmon 27695 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈
No → dom 𝑆
∈ On) |
| 125 | 74, 124 | syl 17 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → dom 𝑆 ∈ On) |
| 126 | | sltres 27707 |
. . . . . . . . . . . . 13
⊢ ((𝑍 ∈
No ∧ 𝑏 ∈
No ∧ dom 𝑆 ∈ On) → ((𝑍 ↾ dom 𝑆) <s (𝑏 ↾ dom 𝑆) → 𝑍 <s 𝑏)) |
| 127 | 89, 91, 125, 126 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆) <s (𝑏 ↾ dom 𝑆) → 𝑍 <s 𝑏)) |
| 128 | 123, 127 | sylbird 260 |
. . . . . . . . . . 11
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑆 <s (𝑏 ↾ dom 𝑆) → 𝑍 <s 𝑏)) |
| 129 | | simplrr 778 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → ¬ (𝑏 ↾ dom 𝑆) <s 𝑆) |
| 130 | 129 | adantr 480 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ¬ (𝑏 ↾ dom 𝑆) <s 𝑆) |
| 131 | | noreson 27705 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈
No ∧ dom 𝑆
∈ On) → (𝑏
↾ dom 𝑆) ∈ No ) |
| 132 | 91, 125, 131 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑏 ↾ dom 𝑆) ∈ No
) |
| 133 | | sltso 27721 |
. . . . . . . . . . . . . . 15
⊢ <s Or
No |
| 134 | | sotric 5622 |
. . . . . . . . . . . . . . 15
⊢ (( <s
Or No ∧ ((𝑏 ↾ dom 𝑆) ∈ No
∧ 𝑆 ∈ No )) → ((𝑏 ↾ dom 𝑆) <s 𝑆 ↔ ¬ ((𝑏 ↾ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑏 ↾ dom 𝑆)))) |
| 135 | 133, 134 | mpan 690 |
. . . . . . . . . . . . . 14
⊢ (((𝑏 ↾ dom 𝑆) ∈ No
∧ 𝑆 ∈ No ) → ((𝑏 ↾ dom 𝑆) <s 𝑆 ↔ ¬ ((𝑏 ↾ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑏 ↾ dom 𝑆)))) |
| 136 | 132, 74, 135 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) <s 𝑆 ↔ ¬ ((𝑏 ↾ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑏 ↾ dom 𝑆)))) |
| 137 | 136 | con2bid 354 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (((𝑏 ↾ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑏 ↾ dom 𝑆)) ↔ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) |
| 138 | 130, 137 | mpbird 257 |
. . . . . . . . . . 11
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑏 ↾ dom 𝑆))) |
| 139 | 122, 128,
138 | mpjaod 861 |
. . . . . . . . . 10
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → 𝑍 <s 𝑏) |
| 140 | 88 | adantr 480 |
. . . . . . . . . . 11
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑍 ∈ No
) |
| 141 | 90 | adantr 480 |
. . . . . . . . . . 11
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑏 ∈ No
) |
| 142 | | simplr 769 |
. . . . . . . . . . 11
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑍 ≠ 𝑏) |
| 143 | 42 | fveq1i 6907 |
. . . . . . . . . . . . 13
⊢ (𝑍‘∩ {𝑝
∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = ((𝑆 ∪ ((suc ∪
( bday “ 𝐵) ∖ dom 𝑆) × {1o}))‘∩ {𝑝
∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) |
| 144 | | simp-4l 783 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (𝐴 ⊆ No
∧ 𝐴 ∈
V)) |
| 145 | 144, 72, 75 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → Fun 𝑆) |
| 146 | | funfn 6596 |
. . . . . . . . . . . . . . 15
⊢ (Fun
𝑆 ↔ 𝑆 Fn dom 𝑆) |
| 147 | 145, 146 | sylib 218 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑆 Fn dom 𝑆) |
| 148 | 46 | fconst 6794 |
. . . . . . . . . . . . . . . 16
⊢ ((suc
∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}):(suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)⟶{1o} |
| 149 | | ffn 6736 |
. . . . . . . . . . . . . . . 16
⊢ (((suc
∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}):(suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)⟶{1o} → ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}) Fn (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)) |
| 150 | 148, 149 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ ((suc
∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}) Fn (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) |
| 151 | 150 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ((suc ∪
( bday “ 𝐵) ∖ dom 𝑆) × {1o}) Fn (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)) |
| 152 | | disjdif 4472 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝑆 ∩ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)) = ∅ |
| 153 | 152 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (dom 𝑆 ∩ (suc ∪
( bday “ 𝐵) ∖ dom 𝑆)) = ∅) |
| 154 | | necom 2994 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑍‘𝑝) ≠ (𝑏‘𝑝) ↔ (𝑏‘𝑝) ≠ (𝑍‘𝑝)) |
| 155 | 154 | rabbii 3442 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} = {𝑝 ∈ On ∣ (𝑏‘𝑝) ≠ (𝑍‘𝑝)} |
| 156 | 155 | inteqi 4950 |
. . . . . . . . . . . . . . . . 17
⊢ ∩ {𝑝
∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} = ∩ {𝑝 ∈ On ∣ (𝑏‘𝑝) ≠ (𝑍‘𝑝)} |
| 157 | 142 | necomd 2996 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑏 ≠ 𝑍) |
| 158 | | nosepssdm 27731 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑏 ∈
No ∧ 𝑍 ∈
No ∧ 𝑏 ≠ 𝑍) → ∩ {𝑝 ∈ On ∣ (𝑏‘𝑝) ≠ (𝑍‘𝑝)} ⊆ dom 𝑏) |
| 159 | 141, 140,
157, 158 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ∩
{𝑝 ∈ On ∣ (𝑏‘𝑝) ≠ (𝑍‘𝑝)} ⊆ dom 𝑏) |
| 160 | 156, 159 | eqsstrid 4022 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ∩
{𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ⊆ dom 𝑏) |
| 161 | 141, 16 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ( bday
‘𝑏) = dom
𝑏) |
| 162 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝐵 ⊆ No
) |
| 163 | 162 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝐵 ⊆ No
) |
| 164 | 163 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝐵 ⊆ No
) |
| 165 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝑏 ∈ 𝐵) |
| 166 | 165 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑏 ∈ 𝐵) |
| 167 | 164, 166,
22 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ( bday
‘𝑏) ∈
( bday “ 𝐵)) |
| 168 | 161, 167 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → dom 𝑏 ∈ ( bday
“ 𝐵)) |
| 169 | 168, 25 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → dom 𝑏 ⊆ ∪ ( bday “ 𝐵)) |
| 170 | 141, 27, 35 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (dom 𝑏 ⊆ ∪ ( bday “ 𝐵) ↔ dom 𝑏 ∈ suc ∪
( bday “ 𝐵))) |
| 171 | 169, 170 | mpbid 232 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → dom 𝑏 ∈ suc ∪
( bday “ 𝐵)) |
| 172 | | nosepon 27710 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑍 ∈
No ∧ 𝑏 ∈
No ∧ 𝑍 ≠ 𝑏) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ On) |
| 173 | 140, 141,
142, 172 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ∩
{𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ On) |
| 174 | | eloni 6394 |
. . . . . . . . . . . . . . . . 17
⊢ (∩ {𝑝
∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ On → Ord ∩ {𝑝
∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) |
| 175 | | ordsuc 7833 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Ord
∪ ( bday “ 𝐵) ↔ Ord suc ∪ ( bday “ 𝐵)) |
| 176 | 33, 175 | mpbi 230 |
. . . . . . . . . . . . . . . . . 18
⊢ Ord suc
∪ ( bday “ 𝐵) |
| 177 | | ordtr2 6428 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Ord
∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∧ Ord suc ∪
( bday “ 𝐵)) → ((∩
{𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ⊆ dom 𝑏 ∧ dom 𝑏 ∈ suc ∪
( bday “ 𝐵)) → ∩
{𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ suc ∪
( bday “ 𝐵))) |
| 178 | 176, 177 | mpan2 691 |
. . . . . . . . . . . . . . . . 17
⊢ (Ord
∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} → ((∩
{𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ⊆ dom 𝑏 ∧ dom 𝑏 ∈ suc ∪
( bday “ 𝐵)) → ∩
{𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ suc ∪
( bday “ 𝐵))) |
| 179 | 173, 174,
178 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ((∩
{𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ⊆ dom 𝑏 ∧ dom 𝑏 ∈ suc ∪
( bday “ 𝐵)) → ∩
{𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ suc ∪
( bday “ 𝐵))) |
| 180 | 160, 171,
179 | mp2and 699 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ∩
{𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ suc ∪
( bday “ 𝐵)) |
| 181 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) |
| 182 | 144, 72, 124 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → dom 𝑆 ∈ On) |
| 183 | | ontri1 6418 |
. . . . . . . . . . . . . . . . 17
⊢ ((dom
𝑆 ∈ On ∧ ∩ {𝑝
∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ On) → (dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ↔ ¬ ∩
{𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆)) |
| 184 | 182, 173,
183 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ↔ ¬ ∩
{𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆)) |
| 185 | 181, 184 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ¬ ∩
{𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) |
| 186 | 180, 185 | eldifd 3962 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ∩
{𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ (suc ∪
( bday “ 𝐵) ∖ dom 𝑆)) |
| 187 | | fvun2 7001 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 Fn dom 𝑆 ∧ ((suc ∪
( bday “ 𝐵) ∖ dom 𝑆) × {1o}) Fn (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) ∧ ((dom 𝑆 ∩ (suc ∪
( bday “ 𝐵) ∖ dom 𝑆)) = ∅ ∧ ∩ {𝑝
∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ (suc ∪
( bday “ 𝐵) ∖ dom 𝑆))) → ((𝑆 ∪ ((suc ∪
( bday “ 𝐵) ∖ dom 𝑆) × {1o}))‘∩ {𝑝
∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (((suc ∪
( bday “ 𝐵) ∖ dom 𝑆) × {1o})‘∩ {𝑝
∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})) |
| 188 | 147, 151,
153, 186, 187 | syl112anc 1376 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ((𝑆 ∪ ((suc ∪
( bday “ 𝐵) ∖ dom 𝑆) × {1o}))‘∩ {𝑝
∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (((suc ∪
( bday “ 𝐵) ∖ dom 𝑆) × {1o})‘∩ {𝑝
∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})) |
| 189 | 143, 188 | eqtrid 2789 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (((suc ∪
( bday “ 𝐵) ∖ dom 𝑆) × {1o})‘∩ {𝑝
∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})) |
| 190 | 46 | fvconst2 7224 |
. . . . . . . . . . . . 13
⊢ (∩ {𝑝
∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ (suc ∪
( bday “ 𝐵) ∖ dom 𝑆) → (((suc ∪
( bday “ 𝐵) ∖ dom 𝑆) × {1o})‘∩ {𝑝
∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = 1o) |
| 191 | 186, 190 | syl 17 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o})‘∩ {𝑝
∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = 1o) |
| 192 | 189, 191 | eqtrd 2777 |
. . . . . . . . . . 11
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = 1o) |
| 193 | | nosep1o 27726 |
. . . . . . . . . . 11
⊢ (((𝑍 ∈
No ∧ 𝑏 ∈
No ∧ 𝑍 ≠ 𝑏) ∧ (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = 1o) → 𝑍 <s 𝑏) |
| 194 | 140, 141,
142, 192, 193 | syl31anc 1375 |
. . . . . . . . . 10
⊢
((((((𝐴 ⊆
No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑍 <s 𝑏) |
| 195 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝑍 ≠ 𝑏) |
| 196 | 88, 90, 195, 172 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ On) |
| 197 | 196, 174 | syl 17 |
. . . . . . . . . . 11
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → Ord ∩
{𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) |
| 198 | | nodmord 27698 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈
No → Ord dom 𝑆) |
| 199 | 71, 72, 198 | 3syl 18 |
. . . . . . . . . . 11
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → Ord dom 𝑆) |
| 200 | | ordtri2or 6482 |
. . . . . . . . . . 11
⊢ ((Ord
∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∧ Ord dom 𝑆) → (∩
{𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆 ∨ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})) |
| 201 | 197, 199,
200 | syl2anc 584 |
. . . . . . . . . 10
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → (∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆 ∨ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})) |
| 202 | 139, 194,
201 | mpjaodan 961 |
. . . . . . . . 9
⊢
(((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ V)) ∧
(𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝑍 <s 𝑏) |
| 203 | 202 | ex 412 |
. . . . . . . 8
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → (𝑍 ≠ 𝑏 → 𝑍 <s 𝑏)) |
| 204 | 56, 203 | biimtrrid 243 |
. . . . . . 7
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → (¬ 𝑍 = 𝑏 → 𝑍 <s 𝑏)) |
| 205 | 55, 204 | mpd 15 |
. . . . . 6
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝑍 <s 𝑏) |
| 206 | 205 | expr 456 |
. . . . 5
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → (¬ (𝑏 ↾ dom 𝑆) <s 𝑆 → 𝑍 <s 𝑏)) |
| 207 | 8, 206 | sylbid 240 |
. . . 4
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑏 → 𝑍 <s 𝑏)) |
| 208 | 207 | ralimdva 3167 |
. . 3
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → (∀𝑏 ∈ 𝐵 ∀𝑎 ∈ 𝐴 𝑎 <s 𝑏 → ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) |
| 209 | 1, 208 | biimtrid 242 |
. 2
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 → ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) |
| 210 | 209 | 3impia 1118 |
1
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) |