Step | Hyp | Ref
| Expression |
1 | | eleq1 2676 |
. . . . 5
⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴)) |
2 | 1 | anbi2d 736 |
. . . 4
⊢ (𝑥 = 𝐵 → ((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) ↔ (Ord 𝐴 ∧ 𝐵 ∈ 𝐴))) |
3 | | ordeq 5647 |
. . . 4
⊢ (𝑥 = 𝐵 → (Ord 𝑥 ↔ Ord 𝐵)) |
4 | 2, 3 | imbi12d 333 |
. . 3
⊢ (𝑥 = 𝐵 → (((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) → Ord 𝑥) ↔ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵))) |
5 | | simpll 786 |
. . . . . . . . 9
⊢ (((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → Ord 𝐴) |
6 | | 3anrot 1036 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) ↔ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴)) |
7 | | 3anass 1035 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥))) |
8 | 6, 7 | bitr3i 265 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥))) |
9 | | ordtr 5654 |
. . . . . . . . . . . 12
⊢ (Ord
𝐴 → Tr 𝐴) |
10 | | trel3 4688 |
. . . . . . . . . . . 12
⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑧 ∈ 𝐴)) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . 11
⊢ (Ord
𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑧 ∈ 𝐴)) |
12 | 8, 11 | syl5bir 232 |
. . . . . . . . . 10
⊢ (Ord
𝐴 → ((𝑥 ∈ 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → 𝑧 ∈ 𝐴)) |
13 | 12 | impl 648 |
. . . . . . . . 9
⊢ (((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → 𝑧 ∈ 𝐴) |
14 | | trel 4687 |
. . . . . . . . . . . . 13
⊢ (Tr 𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴)) |
15 | 9, 14 | syl 17 |
. . . . . . . . . . . 12
⊢ (Ord
𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴)) |
16 | 15 | expcomd 453 |
. . . . . . . . . . 11
⊢ (Ord
𝐴 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴))) |
17 | 16 | imp31 447 |
. . . . . . . . . 10
⊢ (((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐴) |
18 | 17 | adantrl 748 |
. . . . . . . . 9
⊢ (((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ 𝐴) |
19 | | simplr 788 |
. . . . . . . . 9
⊢ (((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → 𝑥 ∈ 𝐴) |
20 | | ordwe 5653 |
. . . . . . . . . 10
⊢ (Ord
𝐴 → E We 𝐴) |
21 | | wetrep 5031 |
. . . . . . . . . 10
⊢ (( E We
𝐴 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) |
22 | 20, 21 | sylan 487 |
. . . . . . . . 9
⊢ ((Ord
𝐴 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) |
23 | 5, 13, 18, 19, 22 | syl13anc 1320 |
. . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) |
24 | 23 | ex 449 |
. . . . . . 7
⊢ ((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))) |
25 | 24 | pm2.43d 51 |
. . . . . 6
⊢ ((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) |
26 | 25 | alrimivv 1843 |
. . . . 5
⊢ ((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) → ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) |
27 | | dftr2 4682 |
. . . . 5
⊢ (Tr 𝑥 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) |
28 | 26, 27 | sylibr 223 |
. . . 4
⊢ ((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) → Tr 𝑥) |
29 | | trss 4689 |
. . . . . . 7
⊢ (Tr 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴)) |
30 | 9, 29 | syl 17 |
. . . . . 6
⊢ (Ord
𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴)) |
31 | | wess 5025 |
. . . . . 6
⊢ (𝑥 ⊆ 𝐴 → ( E We 𝐴 → E We 𝑥)) |
32 | 30, 20, 31 | syl6ci 69 |
. . . . 5
⊢ (Ord
𝐴 → (𝑥 ∈ 𝐴 → E We 𝑥)) |
33 | 32 | imp 444 |
. . . 4
⊢ ((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) → E We 𝑥) |
34 | | df-ord 5643 |
. . . 4
⊢ (Ord
𝑥 ↔ (Tr 𝑥 ∧ E We 𝑥)) |
35 | 28, 33, 34 | sylanbrc 695 |
. . 3
⊢ ((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) → Ord 𝑥) |
36 | 4, 35 | vtoclg 3239 |
. 2
⊢ (𝐵 ∈ 𝐴 → ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)) |
37 | 36 | anabsi7 856 |
1
⊢ ((Ord
𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵) |