Theorem dfon2lem6 36173

Description: Lemma for dfon2 36177. 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 4060	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊊ 𝑆 → 𝑦 ⊆ 𝑆)
2		ssralv 4014	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ 𝑆 → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)))
3	1, 2	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊊ 𝑆 → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)))
4	3	impcom 412	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ∧ 𝑦 ⊊ 𝑆) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥))
5	4	adantrr 729	. . . . . . . . . . . . . 14 ⊢ ((∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥))
6	5	ad2ant2lr 760	. . . . . . . . . . . . 13 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥))
7		psseq2 4053	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑤 → (𝑧 ⊊ 𝑥 ↔ 𝑧 ⊊ 𝑤))
8	7	anbi1d 642	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → ((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) ↔ (𝑧 ⊊ 𝑤 ∧ Tr 𝑧)))
9		elequ2 2164	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
10	8, 9	imbi12d 347	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → (((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ↔ ((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤)))
11	10	albidv 1947	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ↔ ∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤)))
12	11	rspccv 3587	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → (𝑤 ∈ 𝑦 → ∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤)))
13	6, 12	syl 18	. . . . . . . . . . . 12 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (𝑤 ∈ 𝑦 → ∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤)))
14	13	imp 411	. . . . . . . . . . 11 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤))
15		eldifi 4093	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑠 ∈ 𝑆)
16		psseq2 4053	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑠 → (𝑧 ⊊ 𝑥 ↔ 𝑧 ⊊ 𝑠))
17	16	anbi1d 642	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑠 → ((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) ↔ (𝑧 ⊊ 𝑠 ∧ Tr 𝑧)))
18		elequ2 2164	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑠 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑠))
19	17, 18	imbi12d 347	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑠 → (((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ↔ ((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠)))
20	19	albidv 1947	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑠 → (∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ↔ ∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠)))
21	20	rspcv 3586	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠)))
22	15, 21	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠)))
23		psseq1 4052	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑡 → (𝑧 ⊊ 𝑠 ↔ 𝑡 ⊊ 𝑠))
24		treq 5226	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑡 → (Tr 𝑧 ↔ Tr 𝑡))
25	23, 24	anbi12d 643	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑡 → ((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) ↔ (𝑡 ⊊ 𝑠 ∧ Tr 𝑡)))
26		elequ1 2156	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑡 → (𝑧 ∈ 𝑠 ↔ 𝑡 ∈ 𝑠))
27	25, 26	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑡 → (((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) ↔ ((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠)))
28	27	cbvalvw 2063	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) ↔ ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠))
29	22, 28	imbitrdi 254	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠)))
30	29	impcom 412	. . . . . . . . . . . . 13 ⊢ ((∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦)) → ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠))
31	30	ad2ant2l 758	. . . . . . . . . . . 12 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠))
32	31	adantr 485	. . . . . . . . . . 11 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠))
33		vex 3467	. . . . . . . . . . . . 13 ⊢ 𝑤 ∈ V
34		vex 3467	. . . . . . . . . . . . 13 ⊢ 𝑠 ∈ V
35	33, 34	dfon2lem5 36172	. . . . . . . . . . . 12 ⊢ ((∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤) ∧ ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠)) → (𝑤 ∈ 𝑠 ∨ 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤))
36		3orrot 1106	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ 𝑠 ∨ 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤) ↔ (𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠))
37		3orass 1104	. . . . . . . . . . . . . 14 ⊢ ((𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠) ↔ (𝑤 = 𝑠 ∨ (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)))
38	36, 37	bitri 278	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ 𝑠 ∨ 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤) ↔ (𝑤 = 𝑠 ∨ (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)))
39		eleq1a 2864	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 = 𝑠 → 𝑤 ∈ (𝑆 ∖ 𝑦)))
40		elndif 4095	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ 𝑦 → ¬ 𝑤 ∈ (𝑆 ∖ 𝑦))
41	39, 40	nsyli 158	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 ∈ 𝑦 → ¬ 𝑤 = 𝑠))
42	41	imp 411	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 ∈ (𝑆 ∖ 𝑦) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑤 = 𝑠)
43	42	adantll 726	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦)) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑤 = 𝑠)
44	43	adantll 726	. . . . . . . . . . . . . 14 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑤 = 𝑠)
45		orel1 901	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑤 = 𝑠 → ((𝑤 = 𝑠 ∨ (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)) → (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)))
46		trss 5229	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Tr 𝑦 → (𝑤 ∈ 𝑦 → 𝑤 ⊆ 𝑦))
47		eldifn 4094	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → ¬ 𝑠 ∈ 𝑦)
48		ssel 3939	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ⊆ 𝑦 → (𝑠 ∈ 𝑤 → 𝑠 ∈ 𝑦))
49	48	con3d 153	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ⊆ 𝑦 → (¬ 𝑠 ∈ 𝑦 → ¬ 𝑠 ∈ 𝑤))
50	47, 49	syl5com 32	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 ⊆ 𝑦 → ¬ 𝑠 ∈ 𝑤))
51	46, 50	syl9 78	. . . . . . . . . . . . . . . . . . 19 ⊢ (Tr 𝑦 → (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 ∈ 𝑦 → ¬ 𝑠 ∈ 𝑤)))
52	51	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 ∈ 𝑦 → ¬ 𝑠 ∈ 𝑤)))
53	52	imp31 422	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦)) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑠 ∈ 𝑤)
54	53	adantll 726	. . . . . . . . . . . . . . . 16 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑠 ∈ 𝑤)
55		orel1 901	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑠 ∈ 𝑤 → ((𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠) → 𝑤 ∈ 𝑠))
56	54, 55	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ((𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠) → 𝑤 ∈ 𝑠))
57	45, 56	syl9r 79	. . . . . . . . . . . . . 14 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → (¬ 𝑤 = 𝑠 → ((𝑤 = 𝑠 ∨ (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)) → 𝑤 ∈ 𝑠)))
58	44, 57	mpd 16	. . . . . . . . . . . . 13 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ((𝑤 = 𝑠 ∨ (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)) → 𝑤 ∈ 𝑠))
59	38, 58	biimtrid 245	. . . . . . . . . . . 12 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ((𝑤 ∈ 𝑠 ∨ 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤) → 𝑤 ∈ 𝑠))
60	35, 59	syl5 35	. . . . . . . . . . 11 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ((∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤) ∧ ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠)) → 𝑤 ∈ 𝑠))
61	14, 32, 60	mp2and 711	. . . . . . . . . 10 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝑠)
62	61	ex 417	. . . . . . . . 9 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑠))
63	62	ssrdv 3951	. . . . . . . 8 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → 𝑦 ⊆ 𝑠)
64		dfpss2 4050	. . . . . . . . 9 ⊢ (𝑦 ⊊ 𝑠 ↔ (𝑦 ⊆ 𝑠 ∧ ¬ 𝑦 = 𝑠))
65		psseq1 4052	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑦 → (𝑧 ⊊ 𝑠 ↔ 𝑦 ⊊ 𝑠))
66		treq 5226	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑦 → (Tr 𝑧 ↔ Tr 𝑦))
67	65, 66	anbi12d 643	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → ((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) ↔ (𝑦 ⊊ 𝑠 ∧ Tr 𝑦)))
68		elequ1 2156	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝑠 ↔ 𝑦 ∈ 𝑠))
69	67, 68	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑦 → (((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) ↔ ((𝑦 ⊊ 𝑠 ∧ Tr 𝑦) → 𝑦 ∈ 𝑠)))
70	69	spvv 2015	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) → ((𝑦 ⊊ 𝑠 ∧ Tr 𝑦) → 𝑦 ∈ 𝑠))
71	70	expd 420	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) → (𝑦 ⊊ 𝑠 → (Tr 𝑦 → 𝑦 ∈ 𝑠)))
72	71	com23 87	. . . . . . . . . . . . . 14 ⊢ (∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) → (Tr 𝑦 → (𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠)))
73	22, 72	syl6 36	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → (Tr 𝑦 → (𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠))))
74	73	com3l 90	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → (Tr 𝑦 → (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠))))
75	74	adantld 495	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠))))
76	75	adantl 486	. . . . . . . . . 10 ⊢ ((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) → ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠))))
77	76	imp32 423	. . . . . . . . 9 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠))
78	64, 77	biimtrrid 246	. . . . . . . 8 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → ((𝑦 ⊆ 𝑠 ∧ ¬ 𝑦 = 𝑠) → 𝑦 ∈ 𝑠))
79	63, 78	mpand 707	. . . . . . 7 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (¬ 𝑦 = 𝑠 → 𝑦 ∈ 𝑠))
80	79	orrd 876	. . . . . 6 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠))
81	80	anassrs 472	. . . . 5 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦)) → (𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠))
82	81	ralrimiva 3163	. . . 4 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → ∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠))
83		pssdif 4331	. . . . . . 7 ⊢ (𝑦 ⊊ 𝑆 → (𝑆 ∖ 𝑦) ≠ ∅)
84		r19.2z 4462	. . . . . . . 8 ⊢ (((𝑆 ∖ 𝑦) ≠ ∅ ∧ ∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠)) → ∃𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠))
85	84	ex 417	. . . . . . 7 ⊢ ((𝑆 ∖ 𝑦) ≠ ∅ → (∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → ∃𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠)))
86	83, 85	syl 18	. . . . . 6 ⊢ (𝑦 ⊊ 𝑆 → (∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → ∃𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠)))
87	86	ad2antrl 740	. . . . 5 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → ∃𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠)))
88		eleq1w 2852	. . . . . . . . . 10 ⊢ (𝑦 = 𝑠 → (𝑦 ∈ 𝑆 ↔ 𝑠 ∈ 𝑆))
89	15, 88	imbitrrid 249	. . . . . . . . 9 ⊢ (𝑦 = 𝑠 → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆))
90	89	a1i 11	. . . . . . . 8 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (𝑦 = 𝑠 → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆)))
91		trel 5227	. . . . . . . . . . 11 ⊢ (Tr 𝑆 → ((𝑦 ∈ 𝑠 ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ 𝑆))
92	91	expd 420	. . . . . . . . . 10 ⊢ (Tr 𝑆 → (𝑦 ∈ 𝑠 → (𝑠 ∈ 𝑆 → 𝑦 ∈ 𝑆)))
93	15, 92	syl7 75	. . . . . . . . 9 ⊢ (Tr 𝑆 → (𝑦 ∈ 𝑠 → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆)))
94	93	ad2antrr 738	. . . . . . . 8 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (𝑦 ∈ 𝑠 → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆)))
95	90, 94	jaod 872	. . . . . . 7 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → ((𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆)))
96	95	com23 87	. . . . . 6 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (𝑠 ∈ (𝑆 ∖ 𝑦) → ((𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → 𝑦 ∈ 𝑆)))
97	96	rexlimdv 3170	. . . . 5 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (∃𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → 𝑦 ∈ 𝑆))
98	87, 97	syld 48	. . . 4 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → 𝑦 ∈ 𝑆))
99	82, 98	mpd 16	. . 3 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → 𝑦 ∈ 𝑆)
100	99	ex 417	. 2 ⊢ ((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) → ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → 𝑦 ∈ 𝑆))
101	100	alrimiv 1954	1 ⊢ ((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) → ∀𝑦((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → 𝑦 ∈ 𝑆))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∨ wo 860   ∨ w3o 1100  ∀wal 1565   ∈ wcel 2149   ≠ wne 2964  ∀wral 3085  ∃wrex 3095   ∖ cdif 3910   ⊆ wss 3913   ⊊ wpss 3914  ∅c0 4294  Tr wtr 5219

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-pr 5402  ax-un 7730

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-pw 4566  df-sn 4592  df-pr 4594  df-uni 4874  df-iun 4959  df-tr 5220  df-suc 6364

This theorem is referenced by:  dfon2lem7  36174  dfon2lem8  36175