Metamath Proof Explorer

Theorem dfon2lem8

Description: Lemma for dfon2 . The intersection of a nonempty class A of new ordinals is itself a new ordinal and is contained within A (Contributed by Scott Fenton, 26-Feb-2011)

Ref Expression
Assertion dfon2lem8 ⊢A≠∅∧∀x∈A∀yy⊂x∧Tr⁡y→y∈x→∀zz⊂⋂A∧Tr⁡z→z∈⋂A∧⋂A∈A

Proof

Step Hyp Ref Expression
1 vex ⊢x∈V
2 dfon2lem3 ⊢x∈V→∀yy⊂x∧Tr⁡y→y∈x→Tr⁡x∧∀z∈x¬z∈z
3 1 2 ax-mp ⊢∀yy⊂x∧Tr⁡y→y∈x→Tr⁡x∧∀z∈x¬z∈z
4 3 simpld ⊢∀yy⊂x∧Tr⁡y→y∈x→Tr⁡x
5 4 ralimi ⊢∀x∈A∀yy⊂x∧Tr⁡y→y∈x→∀x∈ATr⁡x
6 trint ⊢∀x∈ATr⁡x→Tr⁡⋂A
7 5 6 syl ⊢∀x∈A∀yy⊂x∧Tr⁡y→y∈x→Tr⁡⋂A
8 7 adantl ⊢A≠∅∧∀x∈A∀yy⊂x∧Tr⁡y→y∈x→Tr⁡⋂A
9 1 dfon2lem7 ⊢∀yy⊂x∧Tr⁡y→y∈x→w∈x→∀tt⊂w∧Tr⁡t→t∈w
10 9 alrimiv ⊢∀yy⊂x∧Tr⁡y→y∈x→∀ww∈x→∀tt⊂w∧Tr⁡t→t∈w
11 10 ralimi ⊢∀x∈A∀yy⊂x∧Tr⁡y→y∈x→∀x∈A∀ww∈x→∀tt⊂w∧Tr⁡t→t∈w
12 df-ral ⊢∀x∈A∀ww∈x→∀tt⊂w∧Tr⁡t→t∈w↔∀xx∈A→∀ww∈x→∀tt⊂w∧Tr⁡t→t∈w
13 19.21v ⊢∀wx∈A→w∈x→∀tt⊂w∧Tr⁡t→t∈w↔x∈A→∀ww∈x→∀tt⊂w∧Tr⁡t→t∈w
14 13 albii ⊢∀x∀wx∈A→w∈x→∀tt⊂w∧Tr⁡t→t∈w↔∀xx∈A→∀ww∈x→∀tt⊂w∧Tr⁡t→t∈w
15 12 14 bitr4i ⊢∀x∈A∀ww∈x→∀tt⊂w∧Tr⁡t→t∈w↔∀x∀wx∈A→w∈x→∀tt⊂w∧Tr⁡t→t∈w
16 impexp ⊢x∈A∧w∈x→∀tt⊂w∧Tr⁡t→t∈w↔x∈A→w∈x→∀tt⊂w∧Tr⁡t→t∈w
17 16 2albii ⊢∀x∀wx∈A∧w∈x→∀tt⊂w∧Tr⁡t→t∈w↔∀x∀wx∈A→w∈x→∀tt⊂w∧Tr⁡t→t∈w
18 eluni2 ⊢w∈⋃A↔∃x∈Aw∈x
19 18 biimpi ⊢w∈⋃A→∃x∈Aw∈x
20 19 imim1i ⊢∃x∈Aw∈x→∀tt⊂w∧Tr⁡t→t∈w→w∈⋃A→∀tt⊂w∧Tr⁡t→t∈w
21 20 alimi ⊢∀w∃x∈Aw∈x→∀tt⊂w∧Tr⁡t→t∈w→∀ww∈⋃A→∀tt⊂w∧Tr⁡t→t∈w
22 alcom ⊢∀x∀wx∈A∧w∈x→∀tt⊂w∧Tr⁡t→t∈w↔∀w∀xx∈A∧w∈x→∀tt⊂w∧Tr⁡t→t∈w
23 19.23v ⊢∀xx∈A∧w∈x→∀tt⊂w∧Tr⁡t→t∈w↔∃xx∈A∧w∈x→∀tt⊂w∧Tr⁡t→t∈w
24 df-rex ⊢∃x∈Aw∈x↔∃xx∈A∧w∈x
25 24 imbi1i ⊢∃x∈Aw∈x→∀tt⊂w∧Tr⁡t→t∈w↔∃xx∈A∧w∈x→∀tt⊂w∧Tr⁡t→t∈w
26 23 25 bitr4i ⊢∀xx∈A∧w∈x→∀tt⊂w∧Tr⁡t→t∈w↔∃x∈Aw∈x→∀tt⊂w∧Tr⁡t→t∈w
27 26 albii ⊢∀w∀xx∈A∧w∈x→∀tt⊂w∧Tr⁡t→t∈w↔∀w∃x∈Aw∈x→∀tt⊂w∧Tr⁡t→t∈w
28 22 27 bitri ⊢∀x∀wx∈A∧w∈x→∀tt⊂w∧Tr⁡t→t∈w↔∀w∃x∈Aw∈x→∀tt⊂w∧Tr⁡t→t∈w
29 df-ral ⊢∀w∈⋃A∀tt⊂w∧Tr⁡t→t∈w↔∀ww∈⋃A→∀tt⊂w∧Tr⁡t→t∈w
30 21 28 29 3imtr4i ⊢∀x∀wx∈A∧w∈x→∀tt⊂w∧Tr⁡t→t∈w→∀w∈⋃A∀tt⊂w∧Tr⁡t→t∈w
31 17 30 sylbir ⊢∀x∀wx∈A→w∈x→∀tt⊂w∧Tr⁡t→t∈w→∀w∈⋃A∀tt⊂w∧Tr⁡t→t∈w
32 15 31 sylbi ⊢∀x∈A∀ww∈x→∀tt⊂w∧Tr⁡t→t∈w→∀w∈⋃A∀tt⊂w∧Tr⁡t→t∈w
33 11 32 syl ⊢∀x∈A∀yy⊂x∧Tr⁡y→y∈x→∀w∈⋃A∀tt⊂w∧Tr⁡t→t∈w
34 33 adantl ⊢A≠∅∧∀x∈A∀yy⊂x∧Tr⁡y→y∈x→∀w∈⋃A∀tt⊂w∧Tr⁡t→t∈w
35 intssuni ⊢A≠∅→⋂A⊆⋃A
36 ssralv ⊢⋂A⊆⋃A→∀w∈⋃A∀tt⊂w∧Tr⁡t→t∈w→∀w∈⋂A∀tt⊂w∧Tr⁡t→t∈w
37 35 36 syl ⊢A≠∅→∀w∈⋃A∀tt⊂w∧Tr⁡t→t∈w→∀w∈⋂A∀tt⊂w∧Tr⁡t→t∈w
38 37 adantr ⊢A≠∅∧∀x∈A∀yy⊂x∧Tr⁡y→y∈x→∀w∈⋃A∀tt⊂w∧Tr⁡t→t∈w→∀w∈⋂A∀tt⊂w∧Tr⁡t→t∈w
39 34 38 mpd ⊢A≠∅∧∀x∈A∀yy⊂x∧Tr⁡y→y∈x→∀w∈⋂A∀tt⊂w∧Tr⁡t→t∈w
40 dfon2lem6 ⊢Tr⁡⋂A∧∀w∈⋂A∀tt⊂w∧Tr⁡t→t∈w→∀zz⊂⋂A∧Tr⁡z→z∈⋂A
41 intex ⊢A≠∅↔⋂A∈V
42 dfon2lem3 ⊢⋂A∈V→∀zz⊂⋂A∧Tr⁡z→z∈⋂A→Tr⁡⋂A∧∀t∈⋂A¬t∈t
43 41 42 sylbi ⊢A≠∅→∀zz⊂⋂A∧Tr⁡z→z∈⋂A→Tr⁡⋂A∧∀t∈⋂A¬t∈t
44 43 imp ⊢A≠∅∧∀zz⊂⋂A∧Tr⁡z→z∈⋂A→Tr⁡⋂A∧∀t∈⋂A¬t∈t
45 44 simprd ⊢A≠∅∧∀zz⊂⋂A∧Tr⁡z→z∈⋂A→∀t∈⋂A¬t∈t
46 untelirr ⊢∀t∈⋂A¬t∈t→¬⋂A∈⋂A
47 45 46 syl ⊢A≠∅∧∀zz⊂⋂A∧Tr⁡z→z∈⋂A→¬⋂A∈⋂A
48 47 adantlr ⊢A≠∅∧∀x∈A∀yy⊂x∧Tr⁡y→y∈x∧∀zz⊂⋂A∧Tr⁡z→z∈⋂A→¬⋂A∈⋂A
49 risset ⊢⋂A∈A↔∃t∈At=⋂A
50 49 notbii ⊢¬⋂A∈A↔¬∃t∈At=⋂A
51 ralnex ⊢∀t∈A¬t=⋂A↔¬∃t∈At=⋂A
52 50 51 bitr4i ⊢¬⋂A∈A↔∀t∈A¬t=⋂A
53 eqcom ⊢t=⋂A↔⋂A=t
54 53 notbii ⊢¬t=⋂A↔¬⋂A=t
55 44 simpld ⊢A≠∅∧∀zz⊂⋂A∧Tr⁡z→z∈⋂A→Tr⁡⋂A
56 55 adantlr ⊢A≠∅∧∀x∈A∀yy⊂x∧Tr⁡y→y∈x∧∀zz⊂⋂A∧Tr⁡z→z∈⋂A→Tr⁡⋂A
57 psseq2 ⊢x=t→y⊂x↔y⊂t
58 57 anbi1d ⊢x=t→y⊂x∧Tr⁡y↔y⊂t∧Tr⁡y
59 elequ2 ⊢x=t→y∈x↔y∈t
60 58 59 imbi12d ⊢x=t→y⊂x∧Tr⁡y→y∈x↔y⊂t∧Tr⁡y→y∈t
61 60 albidv ⊢x=t→∀yy⊂x∧Tr⁡y→y∈x↔∀yy⊂t∧Tr⁡y→y∈t
62 61 rspccv ⊢∀x∈A∀yy⊂x∧Tr⁡y→y∈x→t∈A→∀yy⊂t∧Tr⁡y→y∈t
63 62 adantl ⊢A≠∅∧∀x∈A∀yy⊂x∧Tr⁡y→y∈x→t∈A→∀yy⊂t∧Tr⁡y→y∈t
64 intss1 ⊢t∈A→⋂A⊆t
65 dfpss2 ⊢⋂A⊂t↔⋂A⊆t∧¬⋂A=t
66 psseq1 ⊢y=⋂A→y⊂t↔⋂A⊂t
67 treq ⊢y=⋂A→Tr⁡y↔Tr⁡⋂A
68 66 67 anbi12d ⊢y=⋂A→y⊂t∧Tr⁡y↔⋂A⊂t∧Tr⁡⋂A
69 eleq1 ⊢y=⋂A→y∈t↔⋂A∈t
70 68 69 imbi12d ⊢y=⋂A→y⊂t∧Tr⁡y→y∈t↔⋂A⊂t∧Tr⁡⋂A→⋂A∈t
71 70 spcgv ⊢⋂A∈V→∀yy⊂t∧Tr⁡y→y∈t→⋂A⊂t∧Tr⁡⋂A→⋂A∈t
72 41 71 sylbi ⊢A≠∅→∀yy⊂t∧Tr⁡y→y∈t→⋂A⊂t∧Tr⁡⋂A→⋂A∈t
73 72 imp ⊢A≠∅∧∀yy⊂t∧Tr⁡y→y∈t→⋂A⊂t∧Tr⁡⋂A→⋂A∈t
74 73 expd ⊢A≠∅∧∀yy⊂t∧Tr⁡y→y∈t→⋂A⊂t→Tr⁡⋂A→⋂A∈t
75 65 74 biimtrrid ⊢A≠∅∧∀yy⊂t∧Tr⁡y→y∈t→⋂A⊆t∧¬⋂A=t→Tr⁡⋂A→⋂A∈t
76 75 exp4b ⊢A≠∅→∀yy⊂t∧Tr⁡y→y∈t→⋂A⊆t→¬⋂A=t→Tr⁡⋂A→⋂A∈t
77 76 com45 ⊢A≠∅→∀yy⊂t∧Tr⁡y→y∈t→⋂A⊆t→Tr⁡⋂A→¬⋂A=t→⋂A∈t
78 77 com23 ⊢A≠∅→⋂A⊆t→∀yy⊂t∧Tr⁡y→y∈t→Tr⁡⋂A→¬⋂A=t→⋂A∈t
79 64 78 syl5 ⊢A≠∅→t∈A→∀yy⊂t∧Tr⁡y→y∈t→Tr⁡⋂A→¬⋂A=t→⋂A∈t
80 79 adantr ⊢A≠∅∧∀x∈A∀yy⊂x∧Tr⁡y→y∈x→t∈A→∀yy⊂t∧Tr⁡y→y∈t→Tr⁡⋂A→¬⋂A=t→⋂A∈t
81 63 80 mpdd ⊢A≠∅∧∀x∈A∀yy⊂x∧Tr⁡y→y∈x→t∈A→Tr⁡⋂A→¬⋂A=t→⋂A∈t
82 81 adantr ⊢A≠∅∧∀x∈A∀yy⊂x∧Tr⁡y→y∈x∧∀zz⊂⋂A∧Tr⁡z→z∈⋂A→t∈A→Tr⁡⋂A→¬⋂A=t→⋂A∈t
83 56 82 mpid ⊢A≠∅∧∀x∈A∀yy⊂x∧Tr⁡y→y∈x∧∀zz⊂⋂A∧Tr⁡z→z∈⋂A→t∈A→¬⋂A=t→⋂A∈t
84 54 83 syl7bi ⊢A≠∅∧∀x∈A∀yy⊂x∧Tr⁡y→y∈x∧∀zz⊂⋂A∧Tr⁡z→z∈⋂A→t∈A→¬t=⋂A→⋂A∈t
85 84 ralrimiv ⊢A≠∅∧∀x∈A∀yy⊂x∧Tr⁡y→y∈x∧∀zz⊂⋂A∧Tr⁡z→z∈⋂A→∀t∈A¬t=⋂A→⋂A∈t
86 ralim ⊢∀t∈A¬t=⋂A→⋂A∈t→∀t∈A¬t=⋂A→∀t∈A⋂A∈t
87 85 86 syl ⊢A≠∅∧∀x∈A∀yy⊂x∧Tr⁡y→y∈x∧∀zz⊂⋂A∧Tr⁡z→z∈⋂A→∀t∈A¬t=⋂A→∀t∈A⋂A∈t
88 52 87 biimtrid ⊢A≠∅∧∀x∈A∀yy⊂x∧Tr⁡y→y∈x∧∀zz⊂⋂A∧Tr⁡z→z∈⋂A→¬⋂A∈A→∀t∈A⋂A∈t
89 elintg ⊢⋂A∈V→⋂A∈⋂A↔∀t∈A⋂A∈t
90 41 89 sylbi ⊢A≠∅→⋂A∈⋂A↔∀t∈A⋂A∈t
91 90 ad2antrr ⊢A≠∅∧∀x∈A∀yy⊂x∧Tr⁡y→y∈x∧∀zz⊂⋂A∧Tr⁡z→z∈⋂A→⋂A∈⋂A↔∀t∈A⋂A∈t
92 88 91 sylibrd ⊢A≠∅∧∀x∈A∀yy⊂x∧Tr⁡y→y∈x∧∀zz⊂⋂A∧Tr⁡z→z∈⋂A→¬⋂A∈A→⋂A∈⋂A
93 48 92 mt3d ⊢A≠∅∧∀x∈A∀yy⊂x∧Tr⁡y→y∈x∧∀zz⊂⋂A∧Tr⁡z→z∈⋂A→⋂A∈A
94 93 ex ⊢A≠∅∧∀x∈A∀yy⊂x∧Tr⁡y→y∈x→∀zz⊂⋂A∧Tr⁡z→z∈⋂A→⋂A∈A
95 94 ancld ⊢A≠∅∧∀x∈A∀yy⊂x∧Tr⁡y→y∈x→∀zz⊂⋂A∧Tr⁡z→z∈⋂A→∀zz⊂⋂A∧Tr⁡z→z∈⋂A∧⋂A∈A
96 40 95 syl5 ⊢A≠∅∧∀x∈A∀yy⊂x∧Tr⁡y→y∈x→Tr⁡⋂A∧∀w∈⋂A∀tt⊂w∧Tr⁡t→t∈w→∀zz⊂⋂A∧Tr⁡z→z∈⋂A∧⋂A∈A
97 8 39 96 mp2and ⊢A≠∅∧∀x∈A∀yy⊂x∧Tr⁡y→y∈x→∀zz⊂⋂A∧Tr⁡z→z∈⋂A∧⋂A∈A