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 𝐴 ∧ Tr 𝐵 ) → ( 𝐵 ∈ 𝐴 ↔ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴 ) ) )

Proof

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