This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfon2lem6

Description: Lemma for dfon2 . A transitive class of sets satisfying the new definition satisfies the new definition. (Contributed by Scott Fenton, 25-Feb-2011)

Ref Expression
Assertion dfon2lem6 ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) → ∀ 𝑦 ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 pssss ⊢ ( 𝑦 ⊊ 𝑆 → 𝑦 ⊆ 𝑆 )
2 ssralv ⊢ ( 𝑦 ⊆ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) → ∀ 𝑥 ∈ 𝑦 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) )
3 1 2 syl ⊢ ( 𝑦 ⊊ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) → ∀ 𝑥 ∈ 𝑦 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) )
4 3 impcom ⊢ ( ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ∧ 𝑦 ⊊ 𝑆 ) → ∀ 𝑥 ∈ 𝑦 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) )
5 4 adantrr ⊢ ( ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ∧ ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ) → ∀ 𝑥 ∈ 𝑦 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) )
6 5 ad2ant2lr ⊢ ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ∧ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝑦 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) )
7 psseq2 ⊢ ( 𝑥 = 𝑤 → ( 𝑧 ⊊ 𝑥 ↔ 𝑧 ⊊ 𝑤 ) )
8 7 anbi1d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) ↔ ( 𝑧 ⊊ 𝑤 ∧ Tr 𝑧 ) ) )
9 elequ2 ⊢ ( 𝑥 = 𝑤 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤 ) )
10 8 9 imbi12d ⊢ ( 𝑥 = 𝑤 → ( ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ↔ ( ( 𝑧 ⊊ 𝑤 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑤 ) ) )
11 10 albidv ⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑧 ( ( 𝑧 ⊊ 𝑤 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑤 ) ) )
12 11 rspccv ⊢ ( ∀ 𝑥 ∈ 𝑦 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) → ( 𝑤 ∈ 𝑦 → ∀ 𝑧 ( ( 𝑧 ⊊ 𝑤 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑤 ) ) )
13 6 12 syl ⊢ ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ∧ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ) ) → ( 𝑤 ∈ 𝑦 → ∀ 𝑧 ( ( 𝑧 ⊊ 𝑤 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑤 ) ) )
14 13 imp ⊢ ( ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ∧ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ) ) ∧ 𝑤 ∈ 𝑦 ) → ∀ 𝑧 ( ( 𝑧 ⊊ 𝑤 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑤 ) )
15 eldifi ⊢ ( 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) → 𝑠 ∈ 𝑆 )
16 psseq2 ⊢ ( 𝑥 = 𝑠 → ( 𝑧 ⊊ 𝑥 ↔ 𝑧 ⊊ 𝑠 ) )
17 16 anbi1d ⊢ ( 𝑥 = 𝑠 → ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) ↔ ( 𝑧 ⊊ 𝑠 ∧ Tr 𝑧 ) ) )
18 elequ2 ⊢ ( 𝑥 = 𝑠 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑠 ) )
19 17 18 imbi12d ⊢ ( 𝑥 = 𝑠 → ( ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ↔ ( ( 𝑧 ⊊ 𝑠 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑠 ) ) )
20 19 albidv ⊢ ( 𝑥 = 𝑠 → ( ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑧 ( ( 𝑧 ⊊ 𝑠 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑠 ) ) )
21 20 rspcv ⊢ ( 𝑠 ∈ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) → ∀ 𝑧 ( ( 𝑧 ⊊ 𝑠 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑠 ) ) )
22 15 21 syl ⊢ ( 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) → ∀ 𝑧 ( ( 𝑧 ⊊ 𝑠 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑠 ) ) )
23 psseq1 ⊢ ( 𝑧 = 𝑡 → ( 𝑧 ⊊ 𝑠 ↔ 𝑡 ⊊ 𝑠 ) )
24 treq ⊢ ( 𝑧 = 𝑡 → ( Tr 𝑧 ↔ Tr 𝑡 ) )
25 23 24 anbi12d ⊢ ( 𝑧 = 𝑡 → ( ( 𝑧 ⊊ 𝑠 ∧ Tr 𝑧 ) ↔ ( 𝑡 ⊊ 𝑠 ∧ Tr 𝑡 ) ) )
26 elequ1 ⊢ ( 𝑧 = 𝑡 → ( 𝑧 ∈ 𝑠 ↔ 𝑡 ∈ 𝑠 ) )
27 25 26 imbi12d ⊢ ( 𝑧 = 𝑡 → ( ( ( 𝑧 ⊊ 𝑠 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑠 ) ↔ ( ( 𝑡 ⊊ 𝑠 ∧ Tr 𝑡 ) → 𝑡 ∈ 𝑠 ) ) )
28 27 cbvalvw ⊢ ( ∀ 𝑧 ( ( 𝑧 ⊊ 𝑠 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑠 ) ↔ ∀ 𝑡 ( ( 𝑡 ⊊ 𝑠 ∧ Tr 𝑡 ) → 𝑡 ∈ 𝑠 ) )
29 22 28 imbitrdi ⊢ ( 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) → ∀ 𝑡 ( ( 𝑡 ⊊ 𝑠 ∧ Tr 𝑡 ) → 𝑡 ∈ 𝑠 ) ) )
30 29 impcom ⊢ ( ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ∧ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ) → ∀ 𝑡 ( ( 𝑡 ⊊ 𝑠 ∧ Tr 𝑡 ) → 𝑡 ∈ 𝑠 ) )
31 30 ad2ant2l ⊢ ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ∧ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ) ) → ∀ 𝑡 ( ( 𝑡 ⊊ 𝑠 ∧ Tr 𝑡 ) → 𝑡 ∈ 𝑠 ) )
32 31 adantr ⊢ ( ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ∧ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ) ) ∧ 𝑤 ∈ 𝑦 ) → ∀ 𝑡 ( ( 𝑡 ⊊ 𝑠 ∧ Tr 𝑡 ) → 𝑡 ∈ 𝑠 ) )
33 vex ⊢ 𝑤 ∈ V
34 vex ⊢ 𝑠 ∈ V
35 33 34 dfon2lem5 ⊢ ( ( ∀ 𝑧 ( ( 𝑧 ⊊ 𝑤 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑤 ) ∧ ∀ 𝑡 ( ( 𝑡 ⊊ 𝑠 ∧ Tr 𝑡 ) → 𝑡 ∈ 𝑠 ) ) → ( 𝑤 ∈ 𝑠 ∨ 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤 ) )
36 3orrot ⊢ ( ( 𝑤 ∈ 𝑠 ∨ 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤 ) ↔ ( 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠 ) )
37 3orass ⊢ ( ( 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠 ) ↔ ( 𝑤 = 𝑠 ∨ ( 𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠 ) ) )
38 36 37 bitri ⊢ ( ( 𝑤 ∈ 𝑠 ∨ 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤 ) ↔ ( 𝑤 = 𝑠 ∨ ( 𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠 ) ) )
39 eleq1a ⊢ ( 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) → ( 𝑤 = 𝑠 → 𝑤 ∈ ( 𝑆 ∖ 𝑦 ) ) )
40 elndif ⊢ ( 𝑤 ∈ 𝑦 → ¬ 𝑤 ∈ ( 𝑆 ∖ 𝑦 ) )
41 39 40 nsyli ⊢ ( 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) → ( 𝑤 ∈ 𝑦 → ¬ 𝑤 = 𝑠 ) )
42 41 imp ⊢ ( ( 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ∧ 𝑤 ∈ 𝑦 ) → ¬ 𝑤 = 𝑠 )
43 42 adantll ⊢ ( ( ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ∧ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ) ∧ 𝑤 ∈ 𝑦 ) → ¬ 𝑤 = 𝑠 )
44 43 adantll ⊢ ( ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ∧ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ) ) ∧ 𝑤 ∈ 𝑦 ) → ¬ 𝑤 = 𝑠 )
45 orel1 ⊢ ( ¬ 𝑤 = 𝑠 → ( ( 𝑤 = 𝑠 ∨ ( 𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠 ) ) → ( 𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠 ) ) )
46 trss ⊢ ( Tr 𝑦 → ( 𝑤 ∈ 𝑦 → 𝑤 ⊆ 𝑦 ) )
47 eldifn ⊢ ( 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) → ¬ 𝑠 ∈ 𝑦 )
48 ssel ⊢ ( 𝑤 ⊆ 𝑦 → ( 𝑠 ∈ 𝑤 → 𝑠 ∈ 𝑦 ) )
49 48 con3d ⊢ ( 𝑤 ⊆ 𝑦 → ( ¬ 𝑠 ∈ 𝑦 → ¬ 𝑠 ∈ 𝑤 ) )
50 47 49 syl5com ⊢ ( 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) → ( 𝑤 ⊆ 𝑦 → ¬ 𝑠 ∈ 𝑤 ) )
51 46 50 syl9 ⊢ ( Tr 𝑦 → ( 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) → ( 𝑤 ∈ 𝑦 → ¬ 𝑠 ∈ 𝑤 ) ) )
52 51 adantl ⊢ ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) → ( 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) → ( 𝑤 ∈ 𝑦 → ¬ 𝑠 ∈ 𝑤 ) ) )
53 52 imp31 ⊢ ( ( ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ∧ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ) ∧ 𝑤 ∈ 𝑦 ) → ¬ 𝑠 ∈ 𝑤 )
54 53 adantll ⊢ ( ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ∧ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ) ) ∧ 𝑤 ∈ 𝑦 ) → ¬ 𝑠 ∈ 𝑤 )
55 orel1 ⊢ ( ¬ 𝑠 ∈ 𝑤 → ( ( 𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠 ) → 𝑤 ∈ 𝑠 ) )
56 54 55 syl ⊢ ( ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ∧ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ) ) ∧ 𝑤 ∈ 𝑦 ) → ( ( 𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠 ) → 𝑤 ∈ 𝑠 ) )
57 45 56 syl9r ⊢ ( ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ∧ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ) ) ∧ 𝑤 ∈ 𝑦 ) → ( ¬ 𝑤 = 𝑠 → ( ( 𝑤 = 𝑠 ∨ ( 𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠 ) ) → 𝑤 ∈ 𝑠 ) ) )
58 44 57 mpd ⊢ ( ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ∧ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ) ) ∧ 𝑤 ∈ 𝑦 ) → ( ( 𝑤 = 𝑠 ∨ ( 𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠 ) ) → 𝑤 ∈ 𝑠 ) )
59 38 58 biimtrid ⊢ ( ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ∧ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ) ) ∧ 𝑤 ∈ 𝑦 ) → ( ( 𝑤 ∈ 𝑠 ∨ 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤 ) → 𝑤 ∈ 𝑠 ) )
60 35 59 syl5 ⊢ ( ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ∧ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ) ) ∧ 𝑤 ∈ 𝑦 ) → ( ( ∀ 𝑧 ( ( 𝑧 ⊊ 𝑤 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑤 ) ∧ ∀ 𝑡 ( ( 𝑡 ⊊ 𝑠 ∧ Tr 𝑡 ) → 𝑡 ∈ 𝑠 ) ) → 𝑤 ∈ 𝑠 ) )
61 14 32 60 mp2and ⊢ ( ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ∧ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ) ) ∧ 𝑤 ∈ 𝑦 ) → 𝑤 ∈ 𝑠 )
62 61 ex ⊢ ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ∧ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ) ) → ( 𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑠 ) )
63 62 ssrdv ⊢ ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ∧ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ) ) → 𝑦 ⊆ 𝑠 )
64 dfpss2 ⊢ ( 𝑦 ⊊ 𝑠 ↔ ( 𝑦 ⊆ 𝑠 ∧ ¬ 𝑦 = 𝑠 ) )
65 psseq1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 ⊊ 𝑠 ↔ 𝑦 ⊊ 𝑠 ) )
66 treq ⊢ ( 𝑧 = 𝑦 → ( Tr 𝑧 ↔ Tr 𝑦 ) )
67 65 66 anbi12d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 ⊊ 𝑠 ∧ Tr 𝑧 ) ↔ ( 𝑦 ⊊ 𝑠 ∧ Tr 𝑦 ) ) )
68 elequ1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ 𝑠 ↔ 𝑦 ∈ 𝑠 ) )
69 67 68 imbi12d ⊢ ( 𝑧 = 𝑦 → ( ( ( 𝑧 ⊊ 𝑠 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑠 ) ↔ ( ( 𝑦 ⊊ 𝑠 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑠 ) ) )
70 69 spvv ⊢ ( ∀ 𝑧 ( ( 𝑧 ⊊ 𝑠 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑠 ) → ( ( 𝑦 ⊊ 𝑠 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑠 ) )
71 70 expd ⊢ ( ∀ 𝑧 ( ( 𝑧 ⊊ 𝑠 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑠 ) → ( 𝑦 ⊊ 𝑠 → ( Tr 𝑦 → 𝑦 ∈ 𝑠 ) ) )
72 71 com23 ⊢ ( ∀ 𝑧 ( ( 𝑧 ⊊ 𝑠 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑠 ) → ( Tr 𝑦 → ( 𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠 ) ) )
73 22 72 syl6 ⊢ ( 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) → ( Tr 𝑦 → ( 𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠 ) ) ) )
74 73 com3l ⊢ ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) → ( Tr 𝑦 → ( 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) → ( 𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠 ) ) ) )
75 74 adantld ⊢ ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) → ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) → ( 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) → ( 𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠 ) ) ) )
76 75 adantl ⊢ ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) → ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) → ( 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) → ( 𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠 ) ) ) )
77 76 imp32 ⊢ ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ∧ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ) ) → ( 𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠 ) )
78 64 77 biimtrrid ⊢ ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ∧ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ) ) → ( ( 𝑦 ⊆ 𝑠 ∧ ¬ 𝑦 = 𝑠 ) → 𝑦 ∈ 𝑠 ) )
79 63 78 mpand ⊢ ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ∧ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ) ) → ( ¬ 𝑦 = 𝑠 → 𝑦 ∈ 𝑠 ) )
80 79 orrd ⊢ ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ∧ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ) ) → ( 𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠 ) )
81 80 anassrs ⊢ ( ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ) ∧ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ) → ( 𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠 ) )
82 81 ralrimiva ⊢ ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ) → ∀ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ( 𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠 ) )
83 pssdif ⊢ ( 𝑦 ⊊ 𝑆 → ( 𝑆 ∖ 𝑦 ) ≠ ∅ )
84 r19.2z ⊢ ( ( ( 𝑆 ∖ 𝑦 ) ≠ ∅ ∧ ∀ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ( 𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠 ) ) → ∃ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ( 𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠 ) )
85 84 ex ⊢ ( ( 𝑆 ∖ 𝑦 ) ≠ ∅ → ( ∀ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ( 𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠 ) → ∃ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ( 𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠 ) ) )
86 83 85 syl ⊢ ( 𝑦 ⊊ 𝑆 → ( ∀ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ( 𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠 ) → ∃ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ( 𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠 ) ) )
87 86 ad2antrl ⊢ ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ) → ( ∀ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ( 𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠 ) → ∃ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ( 𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠 ) ) )
88 eleq1w ⊢ ( 𝑦 = 𝑠 → ( 𝑦 ∈ 𝑆 ↔ 𝑠 ∈ 𝑆 ) )
89 15 88 imbitrrid ⊢ ( 𝑦 = 𝑠 → ( 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) → 𝑦 ∈ 𝑆 ) )
90 89 a1i ⊢ ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ) → ( 𝑦 = 𝑠 → ( 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) → 𝑦 ∈ 𝑆 ) ) )
91 trel ⊢ ( Tr 𝑆 → ( ( 𝑦 ∈ 𝑠 ∧ 𝑠 ∈ 𝑆 ) → 𝑦 ∈ 𝑆 ) )
92 91 expd ⊢ ( Tr 𝑆 → ( 𝑦 ∈ 𝑠 → ( 𝑠 ∈ 𝑆 → 𝑦 ∈ 𝑆 ) ) )
93 15 92 syl7 ⊢ ( Tr 𝑆 → ( 𝑦 ∈ 𝑠 → ( 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) → 𝑦 ∈ 𝑆 ) ) )
94 93 ad2antrr ⊢ ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ) → ( 𝑦 ∈ 𝑠 → ( 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) → 𝑦 ∈ 𝑆 ) ) )
95 90 94 jaod ⊢ ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ) → ( ( 𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠 ) → ( 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) → 𝑦 ∈ 𝑆 ) ) )
96 95 com23 ⊢ ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ) → ( 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) → ( ( 𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠 ) → 𝑦 ∈ 𝑆 ) ) )
97 96 rexlimdv ⊢ ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ) → ( ∃ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ( 𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠 ) → 𝑦 ∈ 𝑆 ) )
98 87 97 syld ⊢ ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ) → ( ∀ 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) ( 𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠 ) → 𝑦 ∈ 𝑆 ) )
99 82 98 mpd ⊢ ( ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) ∧ ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) ) → 𝑦 ∈ 𝑆 )
100 99 ex ⊢ ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) → ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑆 ) )
101 100 alrimiv ⊢ ( ( Tr 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑥 ) ) → ∀ 𝑦 ( ( 𝑦 ⊊ 𝑆 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑆 ) )