Theorem dfon2lem6 33752

Description: Lemma for dfon2 33756. 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 4035	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊊ 𝑆 → 𝑦 ⊆ 𝑆)
2		ssralv 3992	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ 𝑆 → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)))
3	1, 2	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊊ 𝑆 → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)))
4	3	impcom 408	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ∧ 𝑦 ⊊ 𝑆) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥))
5	4	adantrr 714	. . . . . . . . . . . . . 14 ⊢ ((∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥))
6	5	ad2ant2lr 745	. . . . . . . . . . . . 13 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥))
7		psseq2 4028	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑤 → (𝑧 ⊊ 𝑥 ↔ 𝑧 ⊊ 𝑤))
8	7	anbi1d 630	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → ((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) ↔ (𝑧 ⊊ 𝑤 ∧ Tr 𝑧)))
9		elequ2 2125	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
10	8, 9	imbi12d 345	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → (((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ↔ ((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤)))
11	10	albidv 1927	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ↔ ∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤)))
12	11	rspccv 3558	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → (𝑤 ∈ 𝑦 → ∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤)))
13	6, 12	syl 17	. . . . . . . . . . . 12 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (𝑤 ∈ 𝑦 → ∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤)))
14	13	imp 407	. . . . . . . . . . 11 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤))
15		eldifi 4066	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑠 ∈ 𝑆)
16		psseq2 4028	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑠 → (𝑧 ⊊ 𝑥 ↔ 𝑧 ⊊ 𝑠))
17	16	anbi1d 630	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑠 → ((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) ↔ (𝑧 ⊊ 𝑠 ∧ Tr 𝑧)))
18		elequ2 2125	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑠 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑠))
19	17, 18	imbi12d 345	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑠 → (((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ↔ ((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠)))
20	19	albidv 1927	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑠 → (∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ↔ ∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠)))
21	20	rspcv 3556	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠)))
22	15, 21	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠)))
23		psseq1 4027	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑡 → (𝑧 ⊊ 𝑠 ↔ 𝑡 ⊊ 𝑠))
24		treq 5202	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑡 → (Tr 𝑧 ↔ Tr 𝑡))
25	23, 24	anbi12d 631	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑡 → ((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) ↔ (𝑡 ⊊ 𝑠 ∧ Tr 𝑡)))
26		elequ1 2117	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑡 → (𝑧 ∈ 𝑠 ↔ 𝑡 ∈ 𝑠))
27	25, 26	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑡 → (((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) ↔ ((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠)))
28	27	cbvalvw 2043	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) ↔ ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠))
29	22, 28	syl6ib 250	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠)))
30	29	impcom 408	. . . . . . . . . . . . 13 ⊢ ((∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦)) → ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠))
31	30	ad2ant2l 743	. . . . . . . . . . . 12 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠))
32	31	adantr 481	. . . . . . . . . . 11 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠))
33		vex 3435	. . . . . . . . . . . . 13 ⊢ 𝑤 ∈ V
34		vex 3435	. . . . . . . . . . . . 13 ⊢ 𝑠 ∈ V
35	33, 34	dfon2lem5 33751	. . . . . . . . . . . 12 ⊢ ((∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤) ∧ ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠)) → (𝑤 ∈ 𝑠 ∨ 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤))
36		3orrot 1091	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ 𝑠 ∨ 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤) ↔ (𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠))
37		3orass 1089	. . . . . . . . . . . . . 14 ⊢ ((𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠) ↔ (𝑤 = 𝑠 ∨ (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)))
38	36, 37	bitri 274	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ 𝑠 ∨ 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤) ↔ (𝑤 = 𝑠 ∨ (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)))
39		eleq1a 2836	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 = 𝑠 → 𝑤 ∈ (𝑆 ∖ 𝑦)))
40		elndif 4068	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ 𝑦 → ¬ 𝑤 ∈ (𝑆 ∖ 𝑦))
41	39, 40	nsyli 157	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 ∈ 𝑦 → ¬ 𝑤 = 𝑠))
42	41	imp 407	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 ∈ (𝑆 ∖ 𝑦) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑤 = 𝑠)
43	42	adantll 711	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦)) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑤 = 𝑠)
44	43	adantll 711	. . . . . . . . . . . . . 14 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑤 = 𝑠)
45		orel1 886	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑤 = 𝑠 → ((𝑤 = 𝑠 ∨ (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)) → (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)))
46		trss 5205	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Tr 𝑦 → (𝑤 ∈ 𝑦 → 𝑤 ⊆ 𝑦))
47		eldifn 4067	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → ¬ 𝑠 ∈ 𝑦)
48		ssel 3919	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ⊆ 𝑦 → (𝑠 ∈ 𝑤 → 𝑠 ∈ 𝑦))
49	48	con3d 152	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ⊆ 𝑦 → (¬ 𝑠 ∈ 𝑦 → ¬ 𝑠 ∈ 𝑤))
50	47, 49	syl5com 31	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 ⊆ 𝑦 → ¬ 𝑠 ∈ 𝑤))
51	46, 50	syl9 77	. . . . . . . . . . . . . . . . . . 19 ⊢ (Tr 𝑦 → (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 ∈ 𝑦 → ¬ 𝑠 ∈ 𝑤)))
52	51	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 ∈ 𝑦 → ¬ 𝑠 ∈ 𝑤)))
53	52	imp31 418	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦)) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑠 ∈ 𝑤)
54	53	adantll 711	. . . . . . . . . . . . . . . 16 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑠 ∈ 𝑤)
55		orel1 886	. . . . . . . . . . . . . . . 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 241	. . . . . . . . . . . 12 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ((𝑤 ∈ 𝑠 ∨ 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤) → 𝑤 ∈ 𝑠))
60	35, 59	syl5 34	. . . . . . . . . . 11 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ((∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤) ∧ ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠)) → 𝑤 ∈ 𝑠))
61	14, 32, 60	mp2and 696	. . . . . . . . . 10 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝑠)
62	61	ex 413	. . . . . . . . 9 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑠))
63	62	ssrdv 3932	. . . . . . . 8 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → 𝑦 ⊆ 𝑠)
64		dfpss2 4025	. . . . . . . . 9 ⊢ (𝑦 ⊊ 𝑠 ↔ (𝑦 ⊆ 𝑠 ∧ ¬ 𝑦 = 𝑠))
65		psseq1 4027	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑦 → (𝑧 ⊊ 𝑠 ↔ 𝑦 ⊊ 𝑠))
66		treq 5202	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑦 → (Tr 𝑧 ↔ Tr 𝑦))
67	65, 66	anbi12d 631	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → ((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) ↔ (𝑦 ⊊ 𝑠 ∧ Tr 𝑦)))
68		elequ1 2117	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝑠 ↔ 𝑦 ∈ 𝑠))
69	67, 68	imbi12d 345	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑦 → (((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) ↔ ((𝑦 ⊊ 𝑠 ∧ Tr 𝑦) → 𝑦 ∈ 𝑠)))
70	69	spvv 2004	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) → ((𝑦 ⊊ 𝑠 ∧ Tr 𝑦) → 𝑦 ∈ 𝑠))
71	70	expd 416	. . . . . . . . . . . . . . 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 491	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠))))
76	75	adantl 482	. . . . . . . . . 10 ⊢ ((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) → ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠))))
77	76	imp32 419	. . . . . . . . 9 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠))
78	64, 77	syl5bir 242	. . . . . . . 8 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → ((𝑦 ⊆ 𝑠 ∧ ¬ 𝑦 = 𝑠) → 𝑦 ∈ 𝑠))
79	63, 78	mpand 692	. . . . . . 7 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (¬ 𝑦 = 𝑠 → 𝑦 ∈ 𝑠))
80	79	orrd 860	. . . . . 6 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠))
81	80	anassrs 468	. . . . 5 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦)) → (𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠))
82	81	ralrimiva 3110	. . . 4 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → ∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠))
83		pssdif 4306	. . . . . . 7 ⊢ (𝑦 ⊊ 𝑆 → (𝑆 ∖ 𝑦) ≠ ∅)
84		r19.2z 4431	. . . . . . . 8 ⊢ (((𝑆 ∖ 𝑦) ≠ ∅ ∧ ∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠)) → ∃𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠))
85	84	ex 413	. . . . . . 7 ⊢ ((𝑆 ∖ 𝑦) ≠ ∅ → (∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → ∃𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠)))
86	83, 85	syl 17	. . . . . 6 ⊢ (𝑦 ⊊ 𝑆 → (∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → ∃𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠)))
87	86	ad2antrl 725	. . . . 5 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → ∃𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠)))
88		eleq1w 2823	. . . . . . . . . 10 ⊢ (𝑦 = 𝑠 → (𝑦 ∈ 𝑆 ↔ 𝑠 ∈ 𝑆))
89	15, 88	syl5ibr 245	. . . . . . . . 9 ⊢ (𝑦 = 𝑠 → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆))
90	89	a1i 11	. . . . . . . 8 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (𝑦 = 𝑠 → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆)))
91		trel 5203	. . . . . . . . . . 11 ⊢ (Tr 𝑆 → ((𝑦 ∈ 𝑠 ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ 𝑆))
92	91	expd 416	. . . . . . . . . 10 ⊢ (Tr 𝑆 → (𝑦 ∈ 𝑠 → (𝑠 ∈ 𝑆 → 𝑦 ∈ 𝑆)))
93	15, 92	syl7 74	. . . . . . . . 9 ⊢ (Tr 𝑆 → (𝑦 ∈ 𝑠 → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆)))
94	93	ad2antrr 723	. . . . . . . 8 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (𝑦 ∈ 𝑠 → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆)))
95	90, 94	jaod 856	. . . . . . 7 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → ((𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆)))
96	95	com23 86	. . . . . 6 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (𝑠 ∈ (𝑆 ∖ 𝑦) → ((𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → 𝑦 ∈ 𝑆)))
97	96	rexlimdv 3214	. . . . 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 413	. 2 ⊢ ((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) → ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → 𝑦 ∈ 𝑆))
101	100	alrimiv 1934	1 ⊢ ((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) → ∀𝑦((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → 𝑦 ∈ 𝑆))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∨ wo 844   ∨ w3o 1085  ∀wal 1540   ∈ wcel 2110   ≠ wne 2945  ∀wral 3066  ∃wrex 3067   ∖ cdif 3889   ⊆ wss 3892   ⊊ wpss 3893  ∅c0 4262  Tr wtr 5196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356  ax-un 7580

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-sbc 3721  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-pw 4541  df-sn 4568  df-pr 4570  df-uni 4846  df-iun 4932  df-tr 5197  df-suc 6270

This theorem is referenced by:  dfon2lem7  33753  dfon2lem8  33754