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 ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Tr}{B}\right)\to \left({B}\in {A}↔\left({B}\subseteq {A}\wedge {B}\ne {A}\right)\right)$

Proof

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