Metamath Proof Explorer

Theorem tz7.7

Description: A transitive class belongs to an ordinal class iff it is strictly included in it. Proposition 7.7 of TakeutiZaring p. 37. (Contributed by NM, 5-May-1994)

Ref Expression
Assertion tz7.7 
|- ( ( Ord A /\ Tr B ) -> ( B e. A <-> ( B C_ A /\ B =/= A ) ) )

Proof

Step Hyp Ref Expression
1 ordtr 
 |-  ( Ord A -> Tr A )
2 ordfr 
 |-  ( Ord A -> _E Fr A )
3 tz7.2 
 |-  ( ( Tr A /\ _E Fr A /\ B e. A ) -> ( B C_ A /\ B =/= A ) )
4 3 3exp 
 |-  ( Tr A -> ( _E Fr A -> ( B e. A -> ( B C_ A /\ B =/= A ) ) ) )
5 1 2 4 sylc 
 |-  ( Ord A -> ( B e. A -> ( B C_ A /\ B =/= A ) ) )
6 5 adantr 
 |-  ( ( Ord A /\ Tr B ) -> ( B e. A -> ( B C_ A /\ B =/= A ) ) )
7 pssdifn0 
 |-  ( ( B C_ A /\ B =/= A ) -> ( A \ B ) =/= (/) )
8 difss 
 |-  ( A \ B ) C_ A
9 tz7.5 
 |-  ( ( Ord A /\ ( A \ B ) C_ A /\ ( A \ B ) =/= (/) ) -> E. x e. ( A \ B ) ( ( A \ B ) i^i x ) = (/) )
10 8 9 mp3an2 
 |-  ( ( Ord A /\ ( A \ B ) =/= (/) ) -> E. x e. ( A \ B ) ( ( A \ B ) i^i x ) = (/) )
11 eldifi 
 |-  ( x e. ( A \ B ) -> x e. A )
12 trss 
 |-  ( Tr A -> ( x e. A -> x C_ A ) )
13 difin0ss 
 |-  ( ( ( A \ B ) i^i x ) = (/) -> ( x C_ A -> x C_ B ) )
14 13 com12 
 |-  ( x C_ A -> ( ( ( A \ B ) i^i x ) = (/) -> x C_ B ) )
15 11 12 14 syl56 
 |-  ( Tr A -> ( x e. ( A \ B ) -> ( ( ( A \ B ) i^i x ) = (/) -> x C_ B ) ) )
16 1 15 syl 
 |-  ( Ord A -> ( x e. ( A \ B ) -> ( ( ( A \ B ) i^i x ) = (/) -> x C_ B ) ) )
17 16 ad2antrr 
 |-  ( ( ( Ord A /\ Tr B ) /\ B C_ A ) -> ( x e. ( A \ B ) -> ( ( ( A \ B ) i^i x ) = (/) -> x C_ B ) ) )
18 17 imp32 
 |-  ( ( ( ( Ord A /\ Tr B ) /\ B C_ A ) /\ ( x e. ( A \ B ) /\ ( ( A \ B ) i^i x ) = (/) ) ) -> x C_ B )
19 eleq1w 
 |-  ( y = x -> ( y e. B <-> x e. B ) )
20 19 biimpcd 
 |-  ( y e. B -> ( y = x -> x e. B ) )
21 eldifn 
 |-  ( x e. ( A \ B ) -> -. x e. B )
22 20 21 nsyli 
 |-  ( y e. B -> ( x e. ( A \ B ) -> -. y = x ) )
23 22 imp 
 |-  ( ( y e. B /\ x e. ( A \ B ) ) -> -. y = x )
24 23 adantll 
 |-  ( ( ( B C_ A /\ y e. B ) /\ x e. ( A \ B ) ) -> -. y = x )
25 24 adantl 
 |-  ( ( ( Ord A /\ Tr B ) /\ ( ( B C_ A /\ y e. B ) /\ x e. ( A \ B ) ) ) -> -. y = x )
26 trel 
 |-  ( Tr B -> ( ( x e. y /\ y e. B ) -> x e. B ) )
27 26 expcomd 
 |-  ( Tr B -> ( y e. B -> ( x e. y -> x e. B ) ) )
28 27 imp 
 |-  ( ( Tr B /\ y e. B ) -> ( x e. y -> x e. B ) )
29 28 21 nsyli 
 |-  ( ( Tr B /\ y e. B ) -> ( x e. ( A \ B ) -> -. x e. y ) )
30 29 ex 
 |-  ( Tr B -> ( y e. B -> ( x e. ( A \ B ) -> -. x e. y ) ) )
31 30 adantld 
 |-  ( Tr B -> ( ( B C_ A /\ y e. B ) -> ( x e. ( A \ B ) -> -. x e. y ) ) )
32 31 imp32 
 |-  ( ( Tr B /\ ( ( B C_ A /\ y e. B ) /\ x e. ( A \ B ) ) ) -> -. x e. y )
33 32 adantll 
 |-  ( ( ( Ord A /\ Tr B ) /\ ( ( B C_ A /\ y e. B ) /\ x e. ( A \ B ) ) ) -> -. x e. y )
34 ordwe 
 |-  ( Ord A -> _E We A )
35 ssel2 
 |-  ( ( B C_ A /\ y e. B ) -> y e. A )
36 35 11 anim12i 
 |-  ( ( ( B C_ A /\ y e. B ) /\ x e. ( A \ B ) ) -> ( y e. A /\ x e. A ) )
37 wecmpep 
 |-  ( ( _E We A /\ ( y e. A /\ x e. A ) ) -> ( y e. x \/ y = x \/ x e. y ) )
38 34 36 37 syl2an 
 |-  ( ( Ord A /\ ( ( B C_ A /\ y e. B ) /\ x e. ( A \ B ) ) ) -> ( y e. x \/ y = x \/ x e. y ) )
39 38 adantlr 
 |-  ( ( ( Ord A /\ Tr B ) /\ ( ( B C_ A /\ y e. B ) /\ x e. ( A \ B ) ) ) -> ( y e. x \/ y = x \/ x e. y ) )
40 25 33 39 ecase23d 
 |-  ( ( ( Ord A /\ Tr B ) /\ ( ( B C_ A /\ y e. B ) /\ x e. ( A \ B ) ) ) -> y e. x )
41 40 exp44 
 |-  ( ( Ord A /\ Tr B ) -> ( B C_ A -> ( y e. B -> ( x e. ( A \ B ) -> y e. x ) ) ) )
42 41 com34 
 |-  ( ( Ord A /\ Tr B ) -> ( B C_ A -> ( x e. ( A \ B ) -> ( y e. B -> y e. x ) ) ) )
43 42 imp31 
 |-  ( ( ( ( Ord A /\ Tr B ) /\ B C_ A ) /\ x e. ( A \ B ) ) -> ( y e. B -> y e. x ) )
44 43 ssrdv 
 |-  ( ( ( ( Ord A /\ Tr B ) /\ B C_ A ) /\ x e. ( A \ B ) ) -> B C_ x )
45 44 adantrr 
 |-  ( ( ( ( Ord A /\ Tr B ) /\ B C_ A ) /\ ( x e. ( A \ B ) /\ ( ( A \ B ) i^i x ) = (/) ) ) -> B C_ x )
46 18 45 eqssd 
 |-  ( ( ( ( Ord A /\ Tr B ) /\ B C_ A ) /\ ( x e. ( A \ B ) /\ ( ( A \ B ) i^i x ) = (/) ) ) -> x = B )
47 11 ad2antrl 
 |-  ( ( ( ( Ord A /\ Tr B ) /\ B C_ A ) /\ ( x e. ( A \ B ) /\ ( ( A \ B ) i^i x ) = (/) ) ) -> x e. A )
48 46 47 eqeltrrd 
 |-  ( ( ( ( Ord A /\ Tr B ) /\ B C_ A ) /\ ( x e. ( A \ B ) /\ ( ( A \ B ) i^i x ) = (/) ) ) -> B e. A )
49 48 rexlimdvaa 
 |-  ( ( ( Ord A /\ Tr B ) /\ B C_ A ) -> ( E. x e. ( A \ B ) ( ( A \ B ) i^i x ) = (/) -> B e. A ) )
50 10 49 syl5 
 |-  ( ( ( Ord A /\ Tr B ) /\ B C_ A ) -> ( ( Ord A /\ ( A \ B ) =/= (/) ) -> B e. A ) )
51 50 exp4b 
 |-  ( ( Ord A /\ Tr B ) -> ( B C_ A -> ( Ord A -> ( ( A \ B ) =/= (/) -> B e. A ) ) ) )
52 51 com23 
 |-  ( ( Ord A /\ Tr B ) -> ( Ord A -> ( B C_ A -> ( ( A \ B ) =/= (/) -> B e. A ) ) ) )
53 52 adantrd 
 |-  ( ( Ord A /\ Tr B ) -> ( ( Ord A /\ Tr B ) -> ( B C_ A -> ( ( A \ B ) =/= (/) -> B e. A ) ) ) )
54 53 pm2.43i 
 |-  ( ( Ord A /\ Tr B ) -> ( B C_ A -> ( ( A \ B ) =/= (/) -> B e. A ) ) )
55 7 54 syl7 
 |-  ( ( Ord A /\ Tr B ) -> ( B C_ A -> ( ( B C_ A /\ B =/= A ) -> B e. A ) ) )
56 55 exp4a 
 |-  ( ( Ord A /\ Tr B ) -> ( B C_ A -> ( B C_ A -> ( B =/= A -> B e. A ) ) ) )
57 56 pm2.43d 
 |-  ( ( Ord A /\ Tr B ) -> ( B C_ A -> ( B =/= A -> B e. A ) ) )
58 57 impd 
 |-  ( ( Ord A /\ Tr B ) -> ( ( B C_ A /\ B =/= A ) -> B e. A ) )
59 6 58 impbid 
 |-  ( ( Ord A /\ Tr B ) -> ( B e. A <-> ( B C_ A /\ B =/= A ) ) )