Theorem dfon2lem6 36373

Description: Lemma for dfon2 36377. 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 4049	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊊ 𝑆 → 𝑦 ⊆ 𝑆)
2		ssralv 4003	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ 𝑆 → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)))
3	1, 2	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊊ 𝑆 → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)))
4	3	impcom 413	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ∧ 𝑦 ⊊ 𝑆) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥))
5	4	adantrr 730	. . . . . . . . . . . . . 14 ⊢ ((∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥))
6	5	ad2ant2lr 761	. . . . . . . . . . . . 13 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥))
7		psseq2 4042	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑤 → (𝑧 ⊊ 𝑥 ↔ 𝑧 ⊊ 𝑤))
8	7	anbi1d 643	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → ((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) ↔ (𝑧 ⊊ 𝑤 ∧ Tr 𝑧)))
9		elequ2 2160	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
10	8, 9	imbi12d 347	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → (((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ↔ ((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤)))
11	10	albidv 1953	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ↔ ∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤)))
12	11	rspccv 3576	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → (𝑤 ∈ 𝑦 → ∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤)))
13	6, 12	syl 18	. . . . . . . . . . . 12 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (𝑤 ∈ 𝑦 → ∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤)))
14	13	imp 412	. . . . . . . . . . 11 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤))
15		eldifi 4081	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑠 ∈ 𝑆)
16		psseq2 4042	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑠 → (𝑧 ⊊ 𝑥 ↔ 𝑧 ⊊ 𝑠))
17	16	anbi1d 643	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑠 → ((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) ↔ (𝑧 ⊊ 𝑠 ∧ Tr 𝑧)))
18		elequ2 2160	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑠 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑠))
19	17, 18	imbi12d 347	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑠 → (((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ↔ ((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠)))
20	19	albidv 1953	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑠 → (∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ↔ ∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠)))
21	20	rspcv 3575	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠)))
22	15, 21	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠)))
23		psseq1 4041	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑡 → (𝑧 ⊊ 𝑠 ↔ 𝑡 ⊊ 𝑠))
24		treq 5223	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑡 → (Tr 𝑧 ↔ Tr 𝑡))
25	23, 24	anbi12d 644	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑡 → ((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) ↔ (𝑡 ⊊ 𝑠 ∧ Tr 𝑡)))
26		elequ1 2152	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑡 → (𝑧 ∈ 𝑠 ↔ 𝑡 ∈ 𝑠))
27	25, 26	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑡 → (((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) ↔ ((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠)))
28	27	cbvalvw 2069	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) ↔ ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠))
29	22, 28	imbitrdi 254	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠)))
30	29	impcom 413	. . . . . . . . . . . . 13 ⊢ ((∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦)) → ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠))
31	30	ad2ant2l 759	. . . . . . . . . . . 12 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠))
32	31	adantr 486	. . . . . . . . . . 11 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠))
33		vex 3457	. . . . . . . . . . . . 13 ⊢ 𝑤 ∈ V
34		vex 3457	. . . . . . . . . . . . 13 ⊢ 𝑠 ∈ V
35	33, 34	dfon2lem5 36372	. . . . . . . . . . . 12 ⊢ ((∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤) ∧ ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠)) → (𝑤 ∈ 𝑠 ∨ 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤))
36		3orrot 1108	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ 𝑠 ∨ 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤) ↔ (𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠))
37		3orass 1106	. . . . . . . . . . . . . 14 ⊢ ((𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠) ↔ (𝑤 = 𝑠 ∨ (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)))
38	36, 37	bitri 278	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ 𝑠 ∨ 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤) ↔ (𝑤 = 𝑠 ∨ (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)))
39		eleq1a 2857	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 = 𝑠 → 𝑤 ∈ (𝑆 ∖ 𝑦)))
40		elndif 4083	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ 𝑦 → ¬ 𝑤 ∈ (𝑆 ∖ 𝑦))
41	39, 40	nsyli 158	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 ∈ 𝑦 → ¬ 𝑤 = 𝑠))
42	41	imp 412	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 ∈ (𝑆 ∖ 𝑦) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑤 = 𝑠)
43	42	adantll 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦)) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑤 = 𝑠)
44	43	adantll 727	. . . . . . . . . . . . . 14 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑤 = 𝑠)
45		orel1 902	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑤 = 𝑠 → ((𝑤 = 𝑠 ∨ (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)) → (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)))
46		trss 5226	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Tr 𝑦 → (𝑤 ∈ 𝑦 → 𝑤 ⊆ 𝑦))
47		eldifn 4082	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → ¬ 𝑠 ∈ 𝑦)
48		ssel 3928	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ⊆ 𝑦 → (𝑠 ∈ 𝑤 → 𝑠 ∈ 𝑦))
49	48	con3d 153	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ⊆ 𝑦 → (¬ 𝑠 ∈ 𝑦 → ¬ 𝑠 ∈ 𝑤))
50	47, 49	syl5com 32	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 ⊆ 𝑦 → ¬ 𝑠 ∈ 𝑤))
51	46, 50	syl9 78	. . . . . . . . . . . . . . . . . . 19 ⊢ (Tr 𝑦 → (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 ∈ 𝑦 → ¬ 𝑠 ∈ 𝑤)))
52	51	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 ∈ 𝑦 → ¬ 𝑠 ∈ 𝑤)))
53	52	imp31 423	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦)) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑠 ∈ 𝑤)
54	53	adantll 727	. . . . . . . . . . . . . . . 16 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑠 ∈ 𝑤)
55		orel1 902	. . . . . . . . . . . . . . . 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 712	. . . . . . . . . 10 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝑠)
62	61	ex 418	. . . . . . . . 9 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑠))
63	62	ssrdv 3940	. . . . . . . 8 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → 𝑦 ⊆ 𝑠)
64		dfpss2 4039	. . . . . . . . 9 ⊢ (𝑦 ⊊ 𝑠 ↔ (𝑦 ⊆ 𝑠 ∧ ¬ 𝑦 = 𝑠))
65		psseq1 4041	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑦 → (𝑧 ⊊ 𝑠 ↔ 𝑦 ⊊ 𝑠))
66		treq 5223	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑦 → (Tr 𝑧 ↔ Tr 𝑦))
67	65, 66	anbi12d 644	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → ((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) ↔ (𝑦 ⊊ 𝑠 ∧ Tr 𝑦)))
68		elequ1 2152	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝑠 ↔ 𝑦 ∈ 𝑠))
69	67, 68	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑦 → (((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) ↔ ((𝑦 ⊊ 𝑠 ∧ Tr 𝑦) → 𝑦 ∈ 𝑠)))
70	69	spvv 2021	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) → ((𝑦 ⊊ 𝑠 ∧ Tr 𝑦) → 𝑦 ∈ 𝑠))
71	70	expd 421	. . . . . . . . . . . . . . 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 496	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠))))
76	75	adantl 487	. . . . . . . . . 10 ⊢ ((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) → ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠))))
77	76	imp32 424	. . . . . . . . 9 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠))
78	64, 77	biimtrrid 246	. . . . . . . 8 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → ((𝑦 ⊆ 𝑠 ∧ ¬ 𝑦 = 𝑠) → 𝑦 ∈ 𝑠))
79	63, 78	mpand 708	. . . . . . 7 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (¬ 𝑦 = 𝑠 → 𝑦 ∈ 𝑠))
80	79	orrd 877	. . . . . 6 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠))
81	80	anassrs 473	. . . . 5 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦)) → (𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠))
82	81	ralrimiva 3156	. . . 4 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → ∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠))
83		pssdif 4320	. . . . . . 7 ⊢ (𝑦 ⊊ 𝑆 → (𝑆 ∖ 𝑦) ≠ ∅)
84		r19.2z 4458	. . . . . . . 8 ⊢ (((𝑆 ∖ 𝑦) ≠ ∅ ∧ ∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠)) → ∃𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠))
85	84	ex 418	. . . . . . 7 ⊢ ((𝑆 ∖ 𝑦) ≠ ∅ → (∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → ∃𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠)))
86	83, 85	syl 18	. . . . . 6 ⊢ (𝑦 ⊊ 𝑆 → (∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → ∃𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠)))
87	86	ad2antrl 741	. . . . 5 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → ∃𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠)))
88		eleq1w 2845	. . . . . . . . . 10 ⊢ (𝑦 = 𝑠 → (𝑦 ∈ 𝑆 ↔ 𝑠 ∈ 𝑆))
89	15, 88	imbitrrid 249	. . . . . . . . 9 ⊢ (𝑦 = 𝑠 → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆))
90	89	a1i 11	. . . . . . . 8 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (𝑦 = 𝑠 → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆)))
91		trel 5224	. . . . . . . . . . 11 ⊢ (Tr 𝑆 → ((𝑦 ∈ 𝑠 ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ 𝑆))
92	91	expd 421	. . . . . . . . . 10 ⊢ (Tr 𝑆 → (𝑦 ∈ 𝑠 → (𝑠 ∈ 𝑆 → 𝑦 ∈ 𝑆)))
93	15, 92	syl7 75	. . . . . . . . 9 ⊢ (Tr 𝑆 → (𝑦 ∈ 𝑠 → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆)))
94	93	ad2antrr 739	. . . . . . . 8 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (𝑦 ∈ 𝑠 → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆)))
95	90, 94	jaod 873	. . . . . . 7 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → ((𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆)))
96	95	com23 87	. . . . . 6 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (𝑠 ∈ (𝑆 ∖ 𝑦) → ((𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → 𝑦 ∈ 𝑆)))
97	96	rexlimdv 3163	. . . . 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 418	. 2 ⊢ ((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) → ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → 𝑦 ∈ 𝑆))
101	100	alrimiv 1960	1 ⊢ ((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) → ∀𝑦((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → 𝑦 ∈ 𝑆))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∨ wo 861   ∨ w3o 1102  ∀wal 1568   ∈ wcel 2145   ≠ wne 2957  ∀wral 3078  ∃wrex 3088   ∖ cdif 3899   ⊆ wss 3902   ⊊ wpss 3903  ∅c0 4282  Tr wtr 5216

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-pr 5402  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-pw 4562  df-sn 4588  df-pr 4590  df-uni 4871  df-iun 4956  df-tr 5217  df-suc 6367

This theorem is used by:  dfon2lem7  36374  dfon2lem8  36375