Metamath Proof Explorer

Theorem fin23lem24

Description: Lemma for fin23 . In a class of ordinals, each element is fully identified by those of its predecessors which also belong to the class. (Contributed by Stefan O'Rear, 1-Nov-2014)

Ref Expression
Assertion fin23lem24 ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B → C ∩ B = D ∩ B ↔ C = D

Proof

Step Hyp Ref Expression
1 simpll ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B → Ord ⁡ A
2 simplr ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B → B ⊆ A
3 simprl ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B → C ∈ B
4 2 3 sseldd ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B → C ∈ A
5 ordelord ⊢ Ord ⁡ A ∧ C ∈ A → Ord ⁡ C
6 1 4 5 syl2anc ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B → Ord ⁡ C
7 simprr ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B → D ∈ B
8 2 7 sseldd ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B → D ∈ A
9 ordelord ⊢ Ord ⁡ A ∧ D ∈ A → Ord ⁡ D
10 1 8 9 syl2anc ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B → Ord ⁡ D
11 ordtri3 ⊢ Ord ⁡ C ∧ Ord ⁡ D → C = D ↔ ¬ C ∈ D ∨ D ∈ C
12 11 necon2abid ⊢ Ord ⁡ C ∧ Ord ⁡ D → C ∈ D ∨ D ∈ C ↔ C ≠ D
13 6 10 12 syl2anc ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B → C ∈ D ∨ D ∈ C ↔ C ≠ D
14 simpr ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B ∧ C ∈ D → C ∈ D
15 simplrl ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B ∧ C ∈ D → C ∈ B
16 14 15 elind ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B ∧ C ∈ D → C ∈ D ∩ B
17 6 adantr ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B ∧ C ∈ D → Ord ⁡ C
18 ordirr ⊢ Ord ⁡ C → ¬ C ∈ C
19 17 18 syl ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B ∧ C ∈ D → ¬ C ∈ C
20 elinel1 ⊢ C ∈ C ∩ B → C ∈ C
21 19 20 nsyl ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B ∧ C ∈ D → ¬ C ∈ C ∩ B
22 nelne1 ⊢ C ∈ D ∩ B ∧ ¬ C ∈ C ∩ B → D ∩ B ≠ C ∩ B
23 16 21 22 syl2anc ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B ∧ C ∈ D → D ∩ B ≠ C ∩ B
24 23 necomd ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B ∧ C ∈ D → C ∩ B ≠ D ∩ B
25 simpr ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B ∧ D ∈ C → D ∈ C
26 simplrr ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B ∧ D ∈ C → D ∈ B
27 25 26 elind ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B ∧ D ∈ C → D ∈ C ∩ B
28 10 adantr ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B ∧ D ∈ C → Ord ⁡ D
29 ordirr ⊢ Ord ⁡ D → ¬ D ∈ D
30 28 29 syl ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B ∧ D ∈ C → ¬ D ∈ D
31 elinel1 ⊢ D ∈ D ∩ B → D ∈ D
32 30 31 nsyl ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B ∧ D ∈ C → ¬ D ∈ D ∩ B
33 nelne1 ⊢ D ∈ C ∩ B ∧ ¬ D ∈ D ∩ B → C ∩ B ≠ D ∩ B
34 27 32 33 syl2anc ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B ∧ D ∈ C → C ∩ B ≠ D ∩ B
35 24 34 jaodan ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B ∧ C ∈ D ∨ D ∈ C → C ∩ B ≠ D ∩ B
36 35 ex ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B → C ∈ D ∨ D ∈ C → C ∩ B ≠ D ∩ B
37 13 36 sylbird ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B → C ≠ D → C ∩ B ≠ D ∩ B
38 37 necon4d ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B → C ∩ B = D ∩ B → C = D
39 ineq1 ⊢ C = D → C ∩ B = D ∩ B
40 38 39 impbid1 ⊢ Ord ⁡ A ∧ B ⊆ A ∧ C ∈ B ∧ D ∈ B → C ∩ B = D ∩ B ↔ C = D