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	syl6ib	⊢ ( 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ( ( 𝑧 ⊊ 𝑥 ∧ 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	syl5bi	⊢ ( ( ( ( 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	syl5bir	⊢ ( ( ( 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	syl5ibr	⊢ ( 𝑦 = 𝑠 → ( 𝑠 ∈ ( 𝑆 ∖ 𝑦 ) → 𝑦 ∈ 𝑆 ) )
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 𝑦 ) → 𝑦 ∈ 𝑆 ) )