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 ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) ) → ( ∀ 𝑧 ( ( 𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧 ) → 𝑧 ∈ ∩ 𝐴 ) ∧ ∩ 𝐴 ∈ 𝐴 ) )

Proof

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