Step |
Hyp |
Ref |
Expression |
1 |
|
enrefg |
⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴 ) |
2 |
1
|
adantr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ 𝐴 ) → 𝐴 ≈ 𝐴 ) |
3 |
|
ensn1g |
⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ≈ 1o ) |
4 |
3
|
ensymd |
⊢ ( 𝐴 ∈ 𝑉 → 1o ≈ { 𝐴 } ) |
5 |
4
|
adantr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ 𝐴 ) → 1o ≈ { 𝐴 } ) |
6 |
|
simpr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ 𝐴 ) → ¬ 𝐴 ∈ 𝐴 ) |
7 |
|
disjsn |
⊢ ( ( 𝐴 ∩ { 𝐴 } ) = ∅ ↔ ¬ 𝐴 ∈ 𝐴 ) |
8 |
6 7
|
sylibr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ 𝐴 ) → ( 𝐴 ∩ { 𝐴 } ) = ∅ ) |
9 |
|
djuenun |
⊢ ( ( 𝐴 ≈ 𝐴 ∧ 1o ≈ { 𝐴 } ∧ ( 𝐴 ∩ { 𝐴 } ) = ∅ ) → ( 𝐴 ⊔ 1o ) ≈ ( 𝐴 ∪ { 𝐴 } ) ) |
10 |
2 5 8 9
|
syl3anc |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ 𝐴 ) → ( 𝐴 ⊔ 1o ) ≈ ( 𝐴 ∪ { 𝐴 } ) ) |
11 |
|
df-suc |
⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } ) |
12 |
10 11
|
breqtrrdi |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ 𝐴 ) → ( 𝐴 ⊔ 1o ) ≈ suc 𝐴 ) |