Step | Hyp | Ref
| Expression |
1 | | eleq1 2821 |
. . . . 5
⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴)) |
2 | 1 | anbi2d 632 |
. . . 4
⊢ (𝑥 = 𝐵 → ((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) ↔ (Ord 𝐴 ∧ 𝐵 ∈ 𝐴))) |
3 | | ordeq 6189 |
. . . 4
⊢ (𝑥 = 𝐵 → (Ord 𝑥 ↔ Ord 𝐵)) |
4 | 2, 3 | imbi12d 348 |
. . 3
⊢ (𝑥 = 𝐵 → (((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) → Ord 𝑥) ↔ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵))) |
5 | | simpll 767 |
. . . . . . . . 9
⊢ (((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → Ord 𝐴) |
6 | | 3anrot 1101 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) ↔ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴)) |
7 | | 3anass 1096 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥))) |
8 | 6, 7 | bitr3i 280 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥))) |
9 | | ordtr 6196 |
. . . . . . . . . . . 12
⊢ (Ord
𝐴 → Tr 𝐴) |
10 | | trel3 5154 |
. . . . . . . . . . . 12
⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑧 ∈ 𝐴)) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . 11
⊢ (Ord
𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑧 ∈ 𝐴)) |
12 | 8, 11 | syl5bir 246 |
. . . . . . . . . 10
⊢ (Ord
𝐴 → ((𝑥 ∈ 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → 𝑧 ∈ 𝐴)) |
13 | 12 | impl 459 |
. . . . . . . . 9
⊢ (((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → 𝑧 ∈ 𝐴) |
14 | | trel 5153 |
. . . . . . . . . . . . 13
⊢ (Tr 𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴)) |
15 | 9, 14 | syl 17 |
. . . . . . . . . . . 12
⊢ (Ord
𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴)) |
16 | 15 | expcomd 420 |
. . . . . . . . . . 11
⊢ (Ord
𝐴 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴))) |
17 | 16 | imp31 421 |
. . . . . . . . . 10
⊢ (((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐴) |
18 | 17 | adantrl 716 |
. . . . . . . . 9
⊢ (((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ 𝐴) |
19 | | simplr 769 |
. . . . . . . . 9
⊢ (((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → 𝑥 ∈ 𝐴) |
20 | | ordwe 6195 |
. . . . . . . . . 10
⊢ (Ord
𝐴 → E We 𝐴) |
21 | | wetrep 5528 |
. . . . . . . . . 10
⊢ (( E We
𝐴 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) |
22 | 20, 21 | sylan 583 |
. . . . . . . . 9
⊢ ((Ord
𝐴 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) |
23 | 5, 13, 18, 19, 22 | syl13anc 1373 |
. . . . . . . 8
⊢ (((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) |
24 | 23 | ex 416 |
. . . . . . 7
⊢ ((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))) |
25 | 24 | pm2.43d 53 |
. . . . . 6
⊢ ((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) |
26 | 25 | alrimivv 1935 |
. . . . 5
⊢ ((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) → ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) |
27 | | dftr2 5148 |
. . . . 5
⊢ (Tr 𝑥 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) |
28 | 26, 27 | sylibr 237 |
. . . 4
⊢ ((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) → Tr 𝑥) |
29 | | trss 5155 |
. . . . . . 7
⊢ (Tr 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴)) |
30 | 9, 29 | syl 17 |
. . . . . 6
⊢ (Ord
𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴)) |
31 | | wess 5522 |
. . . . . 6
⊢ (𝑥 ⊆ 𝐴 → ( E We 𝐴 → E We 𝑥)) |
32 | 30, 20, 31 | syl6ci 71 |
. . . . 5
⊢ (Ord
𝐴 → (𝑥 ∈ 𝐴 → E We 𝑥)) |
33 | 32 | imp 410 |
. . . 4
⊢ ((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) → E We 𝑥) |
34 | | df-ord 6185 |
. . . 4
⊢ (Ord
𝑥 ↔ (Tr 𝑥 ∧ E We 𝑥)) |
35 | 28, 33, 34 | sylanbrc 586 |
. . 3
⊢ ((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) → Ord 𝑥) |
36 | 4, 35 | vtoclg 3473 |
. 2
⊢ (𝐵 ∈ 𝐴 → ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)) |
37 | 36 | anabsi7 671 |
1
⊢ ((Ord
𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵) |