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