Theorem dfon2lem6 31693

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

Assertion

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

Distinct variable group:   𝑥,𝑆,𝑦,𝑧

Proof of Theorem dfon2lem6

Dummy variables 𝑤 𝑠 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		pssss 3702	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊊ 𝑆 → 𝑦 ⊆ 𝑆)
2		ssralv 3666	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ 𝑆 → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)))
3	1, 2	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊊ 𝑆 → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)))
4	3	impcom 446	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ∧ 𝑦 ⊊ 𝑆) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥))
5	4	adantrr 753	. . . . . . . . . . . . . 14 ⊢ ((∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥))
6	5	ad2ant2lr 784	. . . . . . . . . . . . 13 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥))
7		psseq2 3695	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑤 → (𝑧 ⊊ 𝑥 ↔ 𝑧 ⊊ 𝑤))
8	7	anbi1d 741	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → ((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) ↔ (𝑧 ⊊ 𝑤 ∧ Tr 𝑧)))
9		elequ2 2004	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
10	8, 9	imbi12d 334	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → (((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ↔ ((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤)))
11	10	albidv 1849	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ↔ ∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤)))
12	11	rspccv 3306	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → (𝑤 ∈ 𝑦 → ∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤)))
13	6, 12	syl 17	. . . . . . . . . . . 12 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (𝑤 ∈ 𝑦 → ∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤)))
14	13	imp 445	. . . . . . . . . . 11 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤))
15		eldifi 3732	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑠 ∈ 𝑆)
16		psseq2 3695	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑠 → (𝑧 ⊊ 𝑥 ↔ 𝑧 ⊊ 𝑠))
17	16	anbi1d 741	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑠 → ((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) ↔ (𝑧 ⊊ 𝑠 ∧ Tr 𝑧)))
18		elequ2 2004	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑠 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑠))
19	17, 18	imbi12d 334	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑠 → (((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ↔ ((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠)))
20	19	albidv 1849	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑠 → (∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ↔ ∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠)))
21	20	rspcv 3305	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠)))
22	15, 21	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠)))
23		psseq1 3694	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑡 → (𝑧 ⊊ 𝑠 ↔ 𝑡 ⊊ 𝑠))
24		treq 4758	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑡 → (Tr 𝑧 ↔ Tr 𝑡))
25	23, 24	anbi12d 747	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑡 → ((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) ↔ (𝑡 ⊊ 𝑠 ∧ Tr 𝑡)))
26		elequ1 1997	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑡 → (𝑧 ∈ 𝑠 ↔ 𝑡 ∈ 𝑠))
27	25, 26	imbi12d 334	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑡 → (((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) ↔ ((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠)))
28	27	cbvalv 2273	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) ↔ ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠))
29	22, 28	syl6ib 241	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠)))
30	29	impcom 446	. . . . . . . . . . . . 13 ⊢ ((∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦)) → ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠))
31	30	ad2ant2l 782	. . . . . . . . . . . 12 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠))
32	31	adantr 481	. . . . . . . . . . 11 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠))
33		vex 3203	. . . . . . . . . . . . 13 ⊢ 𝑤 ∈ V
34		vex 3203	. . . . . . . . . . . . 13 ⊢ 𝑠 ∈ V
35	33, 34	dfon2lem5 31692	. . . . . . . . . . . 12 ⊢ ((∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤) ∧ ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠)) → (𝑤 ∈ 𝑠 ∨ 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤))
36		3orrot 1044	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ 𝑠 ∨ 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤) ↔ (𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠))
37		3orass 1040	. . . . . . . . . . . . . 14 ⊢ ((𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠) ↔ (𝑤 = 𝑠 ∨ (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)))
38	36, 37	bitri 264	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ 𝑠 ∨ 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤) ↔ (𝑤 = 𝑠 ∨ (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)))
39		eleq1a 2696	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 = 𝑠 → 𝑤 ∈ (𝑆 ∖ 𝑦)))
40		elndif 3734	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ 𝑦 → ¬ 𝑤 ∈ (𝑆 ∖ 𝑦))
41	39, 40	nsyli 155	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 ∈ 𝑦 → ¬ 𝑤 = 𝑠))
42	41	imp 445	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 ∈ (𝑆 ∖ 𝑦) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑤 = 𝑠)
43	42	adantll 750	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦)) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑤 = 𝑠)
44	43	adantll 750	. . . . . . . . . . . . . 14 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑤 = 𝑠)
45		orel1 397	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑤 = 𝑠 → ((𝑤 = 𝑠 ∨ (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)) → (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)))
46		trss 4761	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Tr 𝑦 → (𝑤 ∈ 𝑦 → 𝑤 ⊆ 𝑦))
47		eldifn 3733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → ¬ 𝑠 ∈ 𝑦)
48		ssel 3597	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ⊆ 𝑦 → (𝑠 ∈ 𝑤 → 𝑠 ∈ 𝑦))
49	48	con3d 148	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ⊆ 𝑦 → (¬ 𝑠 ∈ 𝑦 → ¬ 𝑠 ∈ 𝑤))
50	47, 49	syl5com 31	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 ⊆ 𝑦 → ¬ 𝑠 ∈ 𝑤))
51	46, 50	syl9 77	. . . . . . . . . . . . . . . . . . 19 ⊢ (Tr 𝑦 → (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 ∈ 𝑦 → ¬ 𝑠 ∈ 𝑤)))
52	51	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 ∈ 𝑦 → ¬ 𝑠 ∈ 𝑤)))
53	52	imp31 448	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦)) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑠 ∈ 𝑤)
54	53	adantll 750	. . . . . . . . . . . . . . . 16 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑠 ∈ 𝑤)
55		orel1 397	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑠 ∈ 𝑤 → ((𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠) → 𝑤 ∈ 𝑠))
56	54, 55	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ((𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠) → 𝑤 ∈ 𝑠))
57	45, 56	syl9r 78	. . . . . . . . . . . . . 14 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → (¬ 𝑤 = 𝑠 → ((𝑤 = 𝑠 ∨ (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)) → 𝑤 ∈ 𝑠)))
58	44, 57	mpd 15	. . . . . . . . . . . . 13 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ((𝑤 = 𝑠 ∨ (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)) → 𝑤 ∈ 𝑠))
59	38, 58	syl5bi 232	. . . . . . . . . . . 12 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ((𝑤 ∈ 𝑠 ∨ 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤) → 𝑤 ∈ 𝑠))
60	35, 59	syl5 34	. . . . . . . . . . 11 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ((∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤) ∧ ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠)) → 𝑤 ∈ 𝑠))
61	14, 32, 60	mp2and 715	. . . . . . . . . 10 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝑠)
62	61	ex 450	. . . . . . . . 9 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑠))
63	62	ssrdv 3609	. . . . . . . 8 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → 𝑦 ⊆ 𝑠)
64		dfpss2 3692	. . . . . . . . 9 ⊢ (𝑦 ⊊ 𝑠 ↔ (𝑦 ⊆ 𝑠 ∧ ¬ 𝑦 = 𝑠))
65		psseq1 3694	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑦 → (𝑧 ⊊ 𝑠 ↔ 𝑦 ⊊ 𝑠))
66		treq 4758	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑦 → (Tr 𝑧 ↔ Tr 𝑦))
67	65, 66	anbi12d 747	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → ((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) ↔ (𝑦 ⊊ 𝑠 ∧ Tr 𝑦)))
68		elequ1 1997	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝑠 ↔ 𝑦 ∈ 𝑠))
69	67, 68	imbi12d 334	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑦 → (((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) ↔ ((𝑦 ⊊ 𝑠 ∧ Tr 𝑦) → 𝑦 ∈ 𝑠)))
70	69	spv 2260	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) → ((𝑦 ⊊ 𝑠 ∧ Tr 𝑦) → 𝑦 ∈ 𝑠))
71	70	expd 452	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) → (𝑦 ⊊ 𝑠 → (Tr 𝑦 → 𝑦 ∈ 𝑠)))
72	71	com23 86	. . . . . . . . . . . . . 14 ⊢ (∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) → (Tr 𝑦 → (𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠)))
73	22, 72	syl6 35	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → (Tr 𝑦 → (𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠))))
74	73	com3l 89	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → (Tr 𝑦 → (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠))))
75	74	adantld 483	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠))))
76	75	adantl 482	. . . . . . . . . 10 ⊢ ((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) → ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠))))
77	76	imp32 449	. . . . . . . . 9 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠))
78	64, 77	syl5bir 233	. . . . . . . 8 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → ((𝑦 ⊆ 𝑠 ∧ ¬ 𝑦 = 𝑠) → 𝑦 ∈ 𝑠))
79	63, 78	mpand 711	. . . . . . 7 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (¬ 𝑦 = 𝑠 → 𝑦 ∈ 𝑠))
80	79	orrd 393	. . . . . 6 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠))
81	80	anassrs 680	. . . . 5 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦)) → (𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠))
82	81	ralrimiva 2966	. . . 4 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → ∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠))
83		pssdif 3945	. . . . . . 7 ⊢ (𝑦 ⊊ 𝑆 → (𝑆 ∖ 𝑦) ≠ ∅)
84		r19.2z 4060	. . . . . . . 8 ⊢ (((𝑆 ∖ 𝑦) ≠ ∅ ∧ ∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠)) → ∃𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠))
85	84	ex 450	. . . . . . 7 ⊢ ((𝑆 ∖ 𝑦) ≠ ∅ → (∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → ∃𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠)))
86	83, 85	syl 17	. . . . . 6 ⊢ (𝑦 ⊊ 𝑆 → (∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → ∃𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠)))
87	86	ad2antrl 764	. . . . 5 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → ∃𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠)))
88		eleq1 2689	. . . . . . . . . 10 ⊢ (𝑦 = 𝑠 → (𝑦 ∈ 𝑆 ↔ 𝑠 ∈ 𝑆))
89	15, 88	syl5ibr 236	. . . . . . . . 9 ⊢ (𝑦 = 𝑠 → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆))
90	89	a1i 11	. . . . . . . 8 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (𝑦 = 𝑠 → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆)))
91		trel 4759	. . . . . . . . . . 11 ⊢ (Tr 𝑆 → ((𝑦 ∈ 𝑠 ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ 𝑆))
92	91	expd 452	. . . . . . . . . 10 ⊢ (Tr 𝑆 → (𝑦 ∈ 𝑠 → (𝑠 ∈ 𝑆 → 𝑦 ∈ 𝑆)))
93	15, 92	syl7 74	. . . . . . . . 9 ⊢ (Tr 𝑆 → (𝑦 ∈ 𝑠 → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆)))
94	93	ad2antrr 762	. . . . . . . 8 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (𝑦 ∈ 𝑠 → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆)))
95	90, 94	jaod 395	. . . . . . 7 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → ((𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆)))
96	95	com23 86	. . . . . 6 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (𝑠 ∈ (𝑆 ∖ 𝑦) → ((𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → 𝑦 ∈ 𝑆)))
97	96	rexlimdv 3030	. . . . 5 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (∃𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → 𝑦 ∈ 𝑆))
98	87, 97	syld 47	. . . 4 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → 𝑦 ∈ 𝑆))
99	82, 98	mpd 15	. . 3 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → 𝑦 ∈ 𝑆)
100	99	ex 450	. 2 ⊢ ((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) → ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → 𝑦 ∈ 𝑆))
101	100	alrimiv 1855	1 ⊢ ((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) → ∀𝑦((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → 𝑦 ∈ 𝑆))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 383   ∧ wa 384   ∨ w3o 1036  ∀wal 1481   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912  ∃wrex 2913   ∖ cdif 3571   ⊆ wss 3574   ⊊ wpss 3575  ∅c0 3915  Tr wtr 4752

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-pw 4160  df-sn 4178  df-pr 4180  df-uni 4437  df-iun 4522  df-tr 4753  df-suc 5729

This theorem is referenced by:  dfon2lem7  31694  dfon2lem8  31695