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 C_ A ) /\ ( C e. B /\ D e. B ) ) -> ( ( C i^i B ) = ( D i^i B ) <-> C = D ) )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) -> Ord A )
2 simplr 
 |-  ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) -> B C_ A )
3 simprl 
 |-  ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) -> C e. B )
4 2 3 sseldd 
 |-  ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) -> C e. A )
5 ordelord 
 |-  ( ( Ord A /\ C e. A ) -> Ord C )
6 1 4 5 syl2anc 
 |-  ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) -> Ord C )
7 simprr 
 |-  ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) -> D e. B )
8 2 7 sseldd 
 |-  ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) -> D e. A )
9 ordelord 
 |-  ( ( Ord A /\ D e. A ) -> Ord D )
10 1 8 9 syl2anc 
 |-  ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) -> Ord D )
11 ordtri3 
 |-  ( ( Ord C /\ Ord D ) -> ( C = D <-> -. ( C e. D \/ D e. C ) ) )
12 11 necon2abid 
 |-  ( ( Ord C /\ Ord D ) -> ( ( C e. D \/ D e. C ) <-> C =/= D ) )
13 6 10 12 syl2anc 
 |-  ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) -> ( ( C e. D \/ D e. C ) <-> C =/= D ) )
14 simpr 
 |-  ( ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) /\ C e. D ) -> C e. D )
15 simplrl 
 |-  ( ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) /\ C e. D ) -> C e. B )
16 14 15 elind 
 |-  ( ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) /\ C e. D ) -> C e. ( D i^i B ) )
17 6 adantr 
 |-  ( ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) /\ C e. D ) -> Ord C )
18 ordirr 
 |-  ( Ord C -> -. C e. C )
19 17 18 syl 
 |-  ( ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) /\ C e. D ) -> -. C e. C )
20 elinel1 
 |-  ( C e. ( C i^i B ) -> C e. C )
21 19 20 nsyl 
 |-  ( ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) /\ C e. D ) -> -. C e. ( C i^i B ) )
22 nelne1 
 |-  ( ( C e. ( D i^i B ) /\ -. C e. ( C i^i B ) ) -> ( D i^i B ) =/= ( C i^i B ) )
23 16 21 22 syl2anc 
 |-  ( ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) /\ C e. D ) -> ( D i^i B ) =/= ( C i^i B ) )
24 23 necomd 
 |-  ( ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) /\ C e. D ) -> ( C i^i B ) =/= ( D i^i B ) )
25 simpr 
 |-  ( ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) /\ D e. C ) -> D e. C )
26 simplrr 
 |-  ( ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) /\ D e. C ) -> D e. B )
27 25 26 elind 
 |-  ( ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) /\ D e. C ) -> D e. ( C i^i B ) )
28 10 adantr 
 |-  ( ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) /\ D e. C ) -> Ord D )
29 ordirr 
 |-  ( Ord D -> -. D e. D )
30 28 29 syl 
 |-  ( ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) /\ D e. C ) -> -. D e. D )
31 elinel1 
 |-  ( D e. ( D i^i B ) -> D e. D )
32 30 31 nsyl 
 |-  ( ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) /\ D e. C ) -> -. D e. ( D i^i B ) )
33 nelne1 
 |-  ( ( D e. ( C i^i B ) /\ -. D e. ( D i^i B ) ) -> ( C i^i B ) =/= ( D i^i B ) )
34 27 32 33 syl2anc 
 |-  ( ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) /\ D e. C ) -> ( C i^i B ) =/= ( D i^i B ) )
35 24 34 jaodan 
 |-  ( ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) /\ ( C e. D \/ D e. C ) ) -> ( C i^i B ) =/= ( D i^i B ) )
36 35 ex 
 |-  ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) -> ( ( C e. D \/ D e. C ) -> ( C i^i B ) =/= ( D i^i B ) ) )
37 13 36 sylbird 
 |-  ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) -> ( C =/= D -> ( C i^i B ) =/= ( D i^i B ) ) )
38 37 necon4d 
 |-  ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) -> ( ( C i^i B ) = ( D i^i B ) -> C = D ) )
39 ineq1 
 |-  ( C = D -> ( C i^i B ) = ( D i^i B ) )
40 38 39 impbid1 
 |-  ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) -> ( ( C i^i B ) = ( D i^i B ) <-> C = D ) )