Step |
Hyp |
Ref |
Expression |
1 |
|
df-ord |
⊢ ( Ord 𝐴 ↔ ( Tr 𝐴 ∧ E We 𝐴 ) ) |
2 |
|
zfregfr |
⊢ E Fr 𝐴 |
3 |
|
dfwe2 |
⊢ ( E We 𝐴 ↔ ( E Fr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥 ) ) ) |
4 |
2 3
|
mpbiran |
⊢ ( E We 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥 ) ) |
5 |
|
epel |
⊢ ( 𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦 ) |
6 |
|
biid |
⊢ ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑦 ) |
7 |
|
epel |
⊢ ( 𝑦 E 𝑥 ↔ 𝑦 ∈ 𝑥 ) |
8 |
5 6 7
|
3orbi123i |
⊢ ( ( 𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥 ) ↔ ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ) |
9 |
8
|
2ralbii |
⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ) |
10 |
4 9
|
bitri |
⊢ ( E We 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ) |
11 |
10
|
anbi2i |
⊢ ( ( Tr 𝐴 ∧ E We 𝐴 ) ↔ ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ) ) |
12 |
1 11
|
bitri |
⊢ ( Ord 𝐴 ↔ ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ) ) |