Step | Hyp | Ref
| Expression |
1 | | ordtr 6277 |
. . . 4
⊢ (Ord
𝐴 → Tr 𝐴) |
2 | | ordfr 6278 |
. . . 4
⊢ (Ord
𝐴 → E Fr 𝐴) |
3 | | tz7.2 5572 |
. . . . 5
⊢ ((Tr
𝐴 ∧ E Fr 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴)) |
4 | 3 | 3exp 1117 |
. . . 4
⊢ (Tr 𝐴 → ( E Fr 𝐴 → (𝐵 ∈ 𝐴 → (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴)))) |
5 | 1, 2, 4 | sylc 65 |
. . 3
⊢ (Ord
𝐴 → (𝐵 ∈ 𝐴 → (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴))) |
6 | 5 | adantr 480 |
. 2
⊢ ((Ord
𝐴 ∧ Tr 𝐵) → (𝐵 ∈ 𝐴 → (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴))) |
7 | | pssdifn0 4304 |
. . . . . 6
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴) → (𝐴 ∖ 𝐵) ≠ ∅) |
8 | | difss 4070 |
. . . . . . . . . . . 12
⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴 |
9 | | tz7.5 6284 |
. . . . . . . . . . . 12
⊢ ((Ord
𝐴 ∧ (𝐴 ∖ 𝐵) ⊆ 𝐴 ∧ (𝐴 ∖ 𝐵) ≠ ∅) → ∃𝑥 ∈ (𝐴 ∖ 𝐵)((𝐴 ∖ 𝐵) ∩ 𝑥) = ∅) |
10 | 8, 9 | mp3an2 1447 |
. . . . . . . . . . 11
⊢ ((Ord
𝐴 ∧ (𝐴 ∖ 𝐵) ≠ ∅) → ∃𝑥 ∈ (𝐴 ∖ 𝐵)((𝐴 ∖ 𝐵) ∩ 𝑥) = ∅) |
11 | | eldifi 4065 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐴) |
12 | | trss 5204 |
. . . . . . . . . . . . . . . . . 18
⊢ (Tr 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴)) |
13 | | difin0ss 4307 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∖ 𝐵) ∩ 𝑥) = ∅ → (𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵)) |
14 | 13 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ⊆ 𝐴 → (((𝐴 ∖ 𝐵) ∩ 𝑥) = ∅ → 𝑥 ⊆ 𝐵)) |
15 | 11, 12, 14 | syl56 36 |
. . . . . . . . . . . . . . . . 17
⊢ (Tr 𝐴 → (𝑥 ∈ (𝐴 ∖ 𝐵) → (((𝐴 ∖ 𝐵) ∩ 𝑥) = ∅ → 𝑥 ⊆ 𝐵))) |
16 | 1, 15 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (Ord
𝐴 → (𝑥 ∈ (𝐴 ∖ 𝐵) → (((𝐴 ∖ 𝐵) ∩ 𝑥) = ∅ → 𝑥 ⊆ 𝐵))) |
17 | 16 | ad2antrr 722 |
. . . . . . . . . . . . . . 15
⊢ (((Ord
𝐴 ∧ Tr 𝐵) ∧ 𝐵 ⊆ 𝐴) → (𝑥 ∈ (𝐴 ∖ 𝐵) → (((𝐴 ∖ 𝐵) ∩ 𝑥) = ∅ → 𝑥 ⊆ 𝐵))) |
18 | 17 | imp32 418 |
. . . . . . . . . . . . . 14
⊢ ((((Ord
𝐴 ∧ Tr 𝐵) ∧ 𝐵 ⊆ 𝐴) ∧ (𝑥 ∈ (𝐴 ∖ 𝐵) ∧ ((𝐴 ∖ 𝐵) ∩ 𝑥) = ∅)) → 𝑥 ⊆ 𝐵) |
19 | | eleq1w 2822 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵)) |
20 | 19 | biimpcd 248 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ 𝐵 → (𝑦 = 𝑥 → 𝑥 ∈ 𝐵)) |
21 | | eldifn 4066 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → ¬ 𝑥 ∈ 𝐵) |
22 | 20, 21 | nsyli 157 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ 𝐵 → (𝑥 ∈ (𝐴 ∖ 𝐵) → ¬ 𝑦 = 𝑥)) |
23 | 22 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) → ¬ 𝑦 = 𝑥) |
24 | 23 | adantll 710 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐵 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) → ¬ 𝑦 = 𝑥) |
25 | 24 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((Ord
𝐴 ∧ Tr 𝐵) ∧ ((𝐵 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵))) → ¬ 𝑦 = 𝑥) |
26 | | trel 5202 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (Tr 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵)) |
27 | 26 | expcomd 416 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (Tr 𝐵 → (𝑦 ∈ 𝐵 → (𝑥 ∈ 𝑦 → 𝑥 ∈ 𝐵))) |
28 | 27 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((Tr
𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝑦 → 𝑥 ∈ 𝐵)) |
29 | 28, 21 | nsyli 157 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((Tr
𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ (𝐴 ∖ 𝐵) → ¬ 𝑥 ∈ 𝑦)) |
30 | 29 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Tr 𝐵 → (𝑦 ∈ 𝐵 → (𝑥 ∈ (𝐴 ∖ 𝐵) → ¬ 𝑥 ∈ 𝑦))) |
31 | 30 | adantld 490 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (Tr 𝐵 → ((𝐵 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ (𝐴 ∖ 𝐵) → ¬ 𝑥 ∈ 𝑦))) |
32 | 31 | imp32 418 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((Tr
𝐵 ∧ ((𝐵 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵))) → ¬ 𝑥 ∈ 𝑦) |
33 | 32 | adantll 710 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((Ord
𝐴 ∧ Tr 𝐵) ∧ ((𝐵 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵))) → ¬ 𝑥 ∈ 𝑦) |
34 | | ordwe 6276 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (Ord
𝐴 → E We 𝐴) |
35 | | ssel2 3920 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐴) |
36 | 35, 11 | anim12i 612 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐵 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) → (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) |
37 | | wecmpep 5580 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (( E We
𝐴 ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (𝑦 ∈ 𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥 ∈ 𝑦)) |
38 | 34, 36, 37 | syl2an 595 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((Ord
𝐴 ∧ ((𝐵 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵))) → (𝑦 ∈ 𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥 ∈ 𝑦)) |
39 | 38 | adantlr 711 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((Ord
𝐴 ∧ Tr 𝐵) ∧ ((𝐵 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵))) → (𝑦 ∈ 𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥 ∈ 𝑦)) |
40 | 25, 33, 39 | ecase23d 1471 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((Ord
𝐴 ∧ Tr 𝐵) ∧ ((𝐵 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵))) → 𝑦 ∈ 𝑥) |
41 | 40 | exp44 437 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Ord
𝐴 ∧ Tr 𝐵) → (𝐵 ⊆ 𝐴 → (𝑦 ∈ 𝐵 → (𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑦 ∈ 𝑥)))) |
42 | 41 | com34 91 |
. . . . . . . . . . . . . . . . 17
⊢ ((Ord
𝐴 ∧ Tr 𝐵) → (𝐵 ⊆ 𝐴 → (𝑥 ∈ (𝐴 ∖ 𝐵) → (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝑥)))) |
43 | 42 | imp31 417 |
. . . . . . . . . . . . . . . 16
⊢ ((((Ord
𝐴 ∧ Tr 𝐵) ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) → (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝑥)) |
44 | 43 | ssrdv 3931 |
. . . . . . . . . . . . . . 15
⊢ ((((Ord
𝐴 ∧ Tr 𝐵) ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) → 𝐵 ⊆ 𝑥) |
45 | 44 | adantrr 713 |
. . . . . . . . . . . . . 14
⊢ ((((Ord
𝐴 ∧ Tr 𝐵) ∧ 𝐵 ⊆ 𝐴) ∧ (𝑥 ∈ (𝐴 ∖ 𝐵) ∧ ((𝐴 ∖ 𝐵) ∩ 𝑥) = ∅)) → 𝐵 ⊆ 𝑥) |
46 | 18, 45 | eqssd 3942 |
. . . . . . . . . . . . 13
⊢ ((((Ord
𝐴 ∧ Tr 𝐵) ∧ 𝐵 ⊆ 𝐴) ∧ (𝑥 ∈ (𝐴 ∖ 𝐵) ∧ ((𝐴 ∖ 𝐵) ∩ 𝑥) = ∅)) → 𝑥 = 𝐵) |
47 | 11 | ad2antrl 724 |
. . . . . . . . . . . . 13
⊢ ((((Ord
𝐴 ∧ Tr 𝐵) ∧ 𝐵 ⊆ 𝐴) ∧ (𝑥 ∈ (𝐴 ∖ 𝐵) ∧ ((𝐴 ∖ 𝐵) ∩ 𝑥) = ∅)) → 𝑥 ∈ 𝐴) |
48 | 46, 47 | eqeltrrd 2841 |
. . . . . . . . . . . 12
⊢ ((((Ord
𝐴 ∧ Tr 𝐵) ∧ 𝐵 ⊆ 𝐴) ∧ (𝑥 ∈ (𝐴 ∖ 𝐵) ∧ ((𝐴 ∖ 𝐵) ∩ 𝑥) = ∅)) → 𝐵 ∈ 𝐴) |
49 | 48 | rexlimdvaa 3215 |
. . . . . . . . . . 11
⊢ (((Ord
𝐴 ∧ Tr 𝐵) ∧ 𝐵 ⊆ 𝐴) → (∃𝑥 ∈ (𝐴 ∖ 𝐵)((𝐴 ∖ 𝐵) ∩ 𝑥) = ∅ → 𝐵 ∈ 𝐴)) |
50 | 10, 49 | syl5 34 |
. . . . . . . . . 10
⊢ (((Ord
𝐴 ∧ Tr 𝐵) ∧ 𝐵 ⊆ 𝐴) → ((Ord 𝐴 ∧ (𝐴 ∖ 𝐵) ≠ ∅) → 𝐵 ∈ 𝐴)) |
51 | 50 | exp4b 430 |
. . . . . . . . 9
⊢ ((Ord
𝐴 ∧ Tr 𝐵) → (𝐵 ⊆ 𝐴 → (Ord 𝐴 → ((𝐴 ∖ 𝐵) ≠ ∅ → 𝐵 ∈ 𝐴)))) |
52 | 51 | com23 86 |
. . . . . . . 8
⊢ ((Ord
𝐴 ∧ Tr 𝐵) → (Ord 𝐴 → (𝐵 ⊆ 𝐴 → ((𝐴 ∖ 𝐵) ≠ ∅ → 𝐵 ∈ 𝐴)))) |
53 | 52 | adantrd 491 |
. . . . . . 7
⊢ ((Ord
𝐴 ∧ Tr 𝐵) → ((Ord 𝐴 ∧ Tr 𝐵) → (𝐵 ⊆ 𝐴 → ((𝐴 ∖ 𝐵) ≠ ∅ → 𝐵 ∈ 𝐴)))) |
54 | 53 | pm2.43i 52 |
. . . . . 6
⊢ ((Ord
𝐴 ∧ Tr 𝐵) → (𝐵 ⊆ 𝐴 → ((𝐴 ∖ 𝐵) ≠ ∅ → 𝐵 ∈ 𝐴))) |
55 | 7, 54 | syl7 74 |
. . . . 5
⊢ ((Ord
𝐴 ∧ Tr 𝐵) → (𝐵 ⊆ 𝐴 → ((𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴) → 𝐵 ∈ 𝐴))) |
56 | 55 | exp4a 431 |
. . . 4
⊢ ((Ord
𝐴 ∧ Tr 𝐵) → (𝐵 ⊆ 𝐴 → (𝐵 ⊆ 𝐴 → (𝐵 ≠ 𝐴 → 𝐵 ∈ 𝐴)))) |
57 | 56 | pm2.43d 53 |
. . 3
⊢ ((Ord
𝐴 ∧ Tr 𝐵) → (𝐵 ⊆ 𝐴 → (𝐵 ≠ 𝐴 → 𝐵 ∈ 𝐴))) |
58 | 57 | impd 410 |
. 2
⊢ ((Ord
𝐴 ∧ Tr 𝐵) → ((𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴) → 𝐵 ∈ 𝐴)) |
59 | 6, 58 | impbid 211 |
1
⊢ ((Ord
𝐴 ∧ Tr 𝐵) → (𝐵 ∈ 𝐴 ↔ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴))) |