| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nodmord 27698 | . . . . . . . 8
⊢ (𝐴 ∈ 
No  → Ord dom 𝐴) | 
| 2 |  | ordirr 6402 | . . . . . . . 8
⊢ (Ord dom
𝐴 → ¬ dom 𝐴 ∈ dom 𝐴) | 
| 3 | 1, 2 | syl 17 | . . . . . . 7
⊢ (𝐴 ∈ 
No  → ¬ dom 𝐴 ∈ dom 𝐴) | 
| 4 |  | ndmfv 6941 | . . . . . . 7
⊢ (¬
dom 𝐴 ∈ dom 𝐴 → (𝐴‘dom 𝐴) = ∅) | 
| 5 | 3, 4 | syl 17 | . . . . . 6
⊢ (𝐴 ∈ 
No  → (𝐴‘dom 𝐴) = ∅) | 
| 6 |  | nofun 27694 | . . . . . . . . 9
⊢ (𝐴 ∈ 
No  → Fun 𝐴) | 
| 7 |  | funfn 6596 | . . . . . . . . 9
⊢ (Fun
𝐴 ↔ 𝐴 Fn dom 𝐴) | 
| 8 | 6, 7 | sylib 218 | . . . . . . . 8
⊢ (𝐴 ∈ 
No  → 𝐴 Fn dom
𝐴) | 
| 9 |  | nodmon 27695 | . . . . . . . . 9
⊢ (𝐴 ∈ 
No  → dom 𝐴
∈ On) | 
| 10 |  | 2on 8520 | . . . . . . . . 9
⊢
2o ∈ On | 
| 11 |  | fnsng 6618 | . . . . . . . . 9
⊢ ((dom
𝐴 ∈ On ∧
2o ∈ On) → {〈dom 𝐴, 2o〉} Fn {dom 𝐴}) | 
| 12 | 9, 10, 11 | sylancl 586 | . . . . . . . 8
⊢ (𝐴 ∈ 
No  → {〈dom 𝐴, 2o〉} Fn {dom 𝐴}) | 
| 13 |  | disjsn 4711 | . . . . . . . . 9
⊢ ((dom
𝐴 ∩ {dom 𝐴}) = ∅ ↔ ¬ dom
𝐴 ∈ dom 𝐴) | 
| 14 | 3, 13 | sylibr 234 | . . . . . . . 8
⊢ (𝐴 ∈ 
No  → (dom 𝐴
∩ {dom 𝐴}) =
∅) | 
| 15 |  | snidg 4660 | . . . . . . . . 9
⊢ (dom
𝐴 ∈ On → dom
𝐴 ∈ {dom 𝐴}) | 
| 16 | 9, 15 | syl 17 | . . . . . . . 8
⊢ (𝐴 ∈ 
No  → dom 𝐴
∈ {dom 𝐴}) | 
| 17 |  | fvun2 7001 | . . . . . . . 8
⊢ ((𝐴 Fn dom 𝐴 ∧ {〈dom 𝐴, 2o〉} Fn {dom 𝐴} ∧ ((dom 𝐴 ∩ {dom 𝐴}) = ∅ ∧ dom 𝐴 ∈ {dom 𝐴})) → ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘dom 𝐴) = ({〈dom 𝐴, 2o〉}‘dom
𝐴)) | 
| 18 | 8, 12, 14, 16, 17 | syl112anc 1376 | . . . . . . 7
⊢ (𝐴 ∈ 
No  → ((𝐴 ∪
{〈dom 𝐴,
2o〉})‘dom 𝐴) = ({〈dom 𝐴, 2o〉}‘dom 𝐴)) | 
| 19 |  | fvsng 7200 | . . . . . . . 8
⊢ ((dom
𝐴 ∈ On ∧
2o ∈ On) → ({〈dom 𝐴, 2o〉}‘dom 𝐴) =
2o) | 
| 20 | 9, 10, 19 | sylancl 586 | . . . . . . 7
⊢ (𝐴 ∈ 
No  → ({〈dom 𝐴, 2o〉}‘dom 𝐴) =
2o) | 
| 21 | 18, 20 | eqtrd 2777 | . . . . . 6
⊢ (𝐴 ∈ 
No  → ((𝐴 ∪
{〈dom 𝐴,
2o〉})‘dom 𝐴) = 2o) | 
| 22 | 5, 21 | jca 511 | . . . . 5
⊢ (𝐴 ∈ 
No  → ((𝐴‘dom 𝐴) = ∅ ∧ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘dom 𝐴) =
2o)) | 
| 23 | 22 | 3mix3d 1339 | . . . 4
⊢ (𝐴 ∈ 
No  → (((𝐴‘dom 𝐴) = 1o ∧ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘dom 𝐴) = ∅) ∨ ((𝐴‘dom 𝐴) = 1o ∧ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘dom 𝐴) = 2o) ∨ ((𝐴‘dom 𝐴) = ∅ ∧ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘dom 𝐴) =
2o))) | 
| 24 |  | fvex 6919 | . . . . 5
⊢ (𝐴‘dom 𝐴) ∈ V | 
| 25 |  | fvex 6919 | . . . . 5
⊢ ((𝐴 ∪ {〈dom 𝐴,
2o〉})‘dom 𝐴) ∈ V | 
| 26 | 24, 25 | brtp 5528 | . . . 4
⊢ ((𝐴‘dom 𝐴){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐴 ∪ {〈dom 𝐴,
2o〉})‘dom 𝐴) ↔ (((𝐴‘dom 𝐴) = 1o ∧ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘dom 𝐴) = ∅) ∨ ((𝐴‘dom 𝐴) = 1o ∧ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘dom 𝐴) = 2o) ∨ ((𝐴‘dom 𝐴) = ∅ ∧ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘dom 𝐴) =
2o))) | 
| 27 | 23, 26 | sylibr 234 | . . 3
⊢ (𝐴 ∈ 
No  → (𝐴‘dom 𝐴){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐴 ∪ {〈dom 𝐴,
2o〉})‘dom 𝐴)) | 
| 28 | 10 | elexi 3503 | . . . . . 6
⊢
2o ∈ V | 
| 29 | 28 | prid2 4763 | . . . . 5
⊢
2o ∈ {1o, 2o} | 
| 30 | 29 | noextenddif 27713 | . . . 4
⊢ (𝐴 ∈ 
No  → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘𝑥)} = dom 𝐴) | 
| 31 | 30 | fveq2d 6910 | . . 3
⊢ (𝐴 ∈ 
No  → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘𝑥)}) = (𝐴‘dom 𝐴)) | 
| 32 | 30 | fveq2d 6910 | . . 3
⊢ (𝐴 ∈ 
No  → ((𝐴 ∪
{〈dom 𝐴,
2o〉})‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘𝑥)}) = ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘dom 𝐴)) | 
| 33 | 27, 31, 32 | 3brtr4d 5175 | . 2
⊢ (𝐴 ∈ 
No  → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘𝑥)}){〈1o,
∅〉, 〈1o, 2o〉, 〈∅,
2o〉} ((𝐴
∪ {〈dom 𝐴,
2o〉})‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘𝑥)})) | 
| 34 | 29 | noextend 27711 | . . 3
⊢ (𝐴 ∈ 
No  → (𝐴 ∪
{〈dom 𝐴,
2o〉}) ∈  No
) | 
| 35 |  | sltval2 27701 | . . 3
⊢ ((𝐴 ∈ 
No  ∧ (𝐴 ∪
{〈dom 𝐴,
2o〉}) ∈  No ) → (𝐴 <s (𝐴 ∪ {〈dom 𝐴, 2o〉}) ↔ (𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘𝑥)}){〈1o,
∅〉, 〈1o, 2o〉, 〈∅,
2o〉} ((𝐴
∪ {〈dom 𝐴,
2o〉})‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘𝑥)}))) | 
| 36 | 34, 35 | mpdan 687 | . 2
⊢ (𝐴 ∈ 
No  → (𝐴 <s
(𝐴 ∪ {〈dom 𝐴, 2o〉}) ↔
(𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘𝑥)}){〈1o,
∅〉, 〈1o, 2o〉, 〈∅,
2o〉} ((𝐴
∪ {〈dom 𝐴,
2o〉})‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘𝑥)}))) | 
| 37 | 33, 36 | mpbird 257 | 1
⊢ (𝐴 ∈ 
No  → 𝐴 <s
(𝐴 ∪ {〈dom 𝐴,
2o〉})) |