This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( ( 𝐶 ∩ 𝐵 ) = ( 𝐷 ∩ 𝐵 ) ↔ 𝐶 = 𝐷 ) )

Proof

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