Proof of Theorem fin23lem24
Step | Hyp | Ref
| Expression |
1 | | simpll 786 |
. . . . . 6
⊢ (((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) → Ord 𝐴) |
2 | | simplr 788 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) → 𝐵 ⊆ 𝐴) |
3 | | simprl 790 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) → 𝐶 ∈ 𝐵) |
4 | 2, 3 | sseldd 3569 |
. . . . . 6
⊢ (((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) → 𝐶 ∈ 𝐴) |
5 | | ordelord 5662 |
. . . . . 6
⊢ ((Ord
𝐴 ∧ 𝐶 ∈ 𝐴) → Ord 𝐶) |
6 | 1, 4, 5 | syl2anc 691 |
. . . . 5
⊢ (((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) → Ord 𝐶) |
7 | | simprr 792 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) → 𝐷 ∈ 𝐵) |
8 | 2, 7 | sseldd 3569 |
. . . . . 6
⊢ (((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) → 𝐷 ∈ 𝐴) |
9 | | ordelord 5662 |
. . . . . 6
⊢ ((Ord
𝐴 ∧ 𝐷 ∈ 𝐴) → Ord 𝐷) |
10 | 1, 8, 9 | syl2anc 691 |
. . . . 5
⊢ (((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) → Ord 𝐷) |
11 | | ordtri3 5676 |
. . . . . 6
⊢ ((Ord
𝐶 ∧ Ord 𝐷) → (𝐶 = 𝐷 ↔ ¬ (𝐶 ∈ 𝐷 ∨ 𝐷 ∈ 𝐶))) |
12 | 11 | necon2abid 2824 |
. . . . 5
⊢ ((Ord
𝐶 ∧ Ord 𝐷) → ((𝐶 ∈ 𝐷 ∨ 𝐷 ∈ 𝐶) ↔ 𝐶 ≠ 𝐷)) |
13 | 6, 10, 12 | syl2anc 691 |
. . . 4
⊢ (((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) → ((𝐶 ∈ 𝐷 ∨ 𝐷 ∈ 𝐶) ↔ 𝐶 ≠ 𝐷)) |
14 | | simpr 476 |
. . . . . . . . 9
⊢ ((((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) ∧ 𝐶 ∈ 𝐷) → 𝐶 ∈ 𝐷) |
15 | | simplrl 796 |
. . . . . . . . 9
⊢ ((((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) ∧ 𝐶 ∈ 𝐷) → 𝐶 ∈ 𝐵) |
16 | 14, 15 | elind 3760 |
. . . . . . . 8
⊢ ((((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) ∧ 𝐶 ∈ 𝐷) → 𝐶 ∈ (𝐷 ∩ 𝐵)) |
17 | 6 | adantr 480 |
. . . . . . . . . 10
⊢ ((((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) ∧ 𝐶 ∈ 𝐷) → Ord 𝐶) |
18 | | ordirr 5658 |
. . . . . . . . . 10
⊢ (Ord
𝐶 → ¬ 𝐶 ∈ 𝐶) |
19 | 17, 18 | syl 17 |
. . . . . . . . 9
⊢ ((((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) ∧ 𝐶 ∈ 𝐷) → ¬ 𝐶 ∈ 𝐶) |
20 | | inss1 3795 |
. . . . . . . . . 10
⊢ (𝐶 ∩ 𝐵) ⊆ 𝐶 |
21 | 20 | sseli 3564 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝐶 ∩ 𝐵) → 𝐶 ∈ 𝐶) |
22 | 19, 21 | nsyl 134 |
. . . . . . . 8
⊢ ((((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) ∧ 𝐶 ∈ 𝐷) → ¬ 𝐶 ∈ (𝐶 ∩ 𝐵)) |
23 | | nelne1 2878 |
. . . . . . . 8
⊢ ((𝐶 ∈ (𝐷 ∩ 𝐵) ∧ ¬ 𝐶 ∈ (𝐶 ∩ 𝐵)) → (𝐷 ∩ 𝐵) ≠ (𝐶 ∩ 𝐵)) |
24 | 16, 22, 23 | syl2anc 691 |
. . . . . . 7
⊢ ((((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) ∧ 𝐶 ∈ 𝐷) → (𝐷 ∩ 𝐵) ≠ (𝐶 ∩ 𝐵)) |
25 | 24 | necomd 2837 |
. . . . . 6
⊢ ((((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) ∧ 𝐶 ∈ 𝐷) → (𝐶 ∩ 𝐵) ≠ (𝐷 ∩ 𝐵)) |
26 | | simpr 476 |
. . . . . . . 8
⊢ ((((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) ∧ 𝐷 ∈ 𝐶) → 𝐷 ∈ 𝐶) |
27 | | simplrr 797 |
. . . . . . . 8
⊢ ((((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) ∧ 𝐷 ∈ 𝐶) → 𝐷 ∈ 𝐵) |
28 | 26, 27 | elind 3760 |
. . . . . . 7
⊢ ((((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) ∧ 𝐷 ∈ 𝐶) → 𝐷 ∈ (𝐶 ∩ 𝐵)) |
29 | 10 | adantr 480 |
. . . . . . . . 9
⊢ ((((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) ∧ 𝐷 ∈ 𝐶) → Ord 𝐷) |
30 | | ordirr 5658 |
. . . . . . . . 9
⊢ (Ord
𝐷 → ¬ 𝐷 ∈ 𝐷) |
31 | 29, 30 | syl 17 |
. . . . . . . 8
⊢ ((((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) ∧ 𝐷 ∈ 𝐶) → ¬ 𝐷 ∈ 𝐷) |
32 | | inss1 3795 |
. . . . . . . . 9
⊢ (𝐷 ∩ 𝐵) ⊆ 𝐷 |
33 | 32 | sseli 3564 |
. . . . . . . 8
⊢ (𝐷 ∈ (𝐷 ∩ 𝐵) → 𝐷 ∈ 𝐷) |
34 | 31, 33 | nsyl 134 |
. . . . . . 7
⊢ ((((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) ∧ 𝐷 ∈ 𝐶) → ¬ 𝐷 ∈ (𝐷 ∩ 𝐵)) |
35 | | nelne1 2878 |
. . . . . . 7
⊢ ((𝐷 ∈ (𝐶 ∩ 𝐵) ∧ ¬ 𝐷 ∈ (𝐷 ∩ 𝐵)) → (𝐶 ∩ 𝐵) ≠ (𝐷 ∩ 𝐵)) |
36 | 28, 34, 35 | syl2anc 691 |
. . . . . 6
⊢ ((((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) ∧ 𝐷 ∈ 𝐶) → (𝐶 ∩ 𝐵) ≠ (𝐷 ∩ 𝐵)) |
37 | 25, 36 | jaodan 822 |
. . . . 5
⊢ ((((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) ∧ (𝐶 ∈ 𝐷 ∨ 𝐷 ∈ 𝐶)) → (𝐶 ∩ 𝐵) ≠ (𝐷 ∩ 𝐵)) |
38 | 37 | ex 449 |
. . . 4
⊢ (((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) → ((𝐶 ∈ 𝐷 ∨ 𝐷 ∈ 𝐶) → (𝐶 ∩ 𝐵) ≠ (𝐷 ∩ 𝐵))) |
39 | 13, 38 | sylbird 249 |
. . 3
⊢ (((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) → (𝐶 ≠ 𝐷 → (𝐶 ∩ 𝐵) ≠ (𝐷 ∩ 𝐵))) |
40 | 39 | necon4d 2806 |
. 2
⊢ (((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) → ((𝐶 ∩ 𝐵) = (𝐷 ∩ 𝐵) → 𝐶 = 𝐷)) |
41 | | ineq1 3769 |
. 2
⊢ (𝐶 = 𝐷 → (𝐶 ∩ 𝐵) = (𝐷 ∩ 𝐵)) |
42 | 40, 41 | impbid1 214 |
1
⊢ (((Ord
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) → ((𝐶 ∩ 𝐵) = (𝐷 ∩ 𝐵) ↔ 𝐶 = 𝐷)) |