Theorem dfon2lem6 35776

Description: Lemma for dfon2 35780. 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 4061	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊊ 𝑆 → 𝑦 ⊆ 𝑆)
2		ssralv 4015	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ 𝑆 → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)))
3	1, 2	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊊ 𝑆 → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)))
4	3	impcom 407	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ∧ 𝑦 ⊊ 𝑆) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥))
5	4	adantrr 717	. . . . . . . . . . . . . 14 ⊢ ((∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥))
6	5	ad2ant2lr 748	. . . . . . . . . . . . 13 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → ∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥))
7		psseq2 4054	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑤 → (𝑧 ⊊ 𝑥 ↔ 𝑧 ⊊ 𝑤))
8	7	anbi1d 631	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → ((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) ↔ (𝑧 ⊊ 𝑤 ∧ Tr 𝑧)))
9		elequ2 2124	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
10	8, 9	imbi12d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → (((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ↔ ((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤)))
11	10	albidv 1920	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ↔ ∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤)))
12	11	rspccv 3585	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ 𝑦 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → (𝑤 ∈ 𝑦 → ∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤)))
13	6, 12	syl 17	. . . . . . . . . . . 12 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (𝑤 ∈ 𝑦 → ∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤)))
14	13	imp 406	. . . . . . . . . . 11 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤))
15		eldifi 4094	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑠 ∈ 𝑆)
16		psseq2 4054	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑠 → (𝑧 ⊊ 𝑥 ↔ 𝑧 ⊊ 𝑠))
17	16	anbi1d 631	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑠 → ((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) ↔ (𝑧 ⊊ 𝑠 ∧ Tr 𝑧)))
18		elequ2 2124	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑠 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑠))
19	17, 18	imbi12d 344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑠 → (((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ↔ ((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠)))
20	19	albidv 1920	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑠 → (∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ↔ ∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠)))
21	20	rspcv 3584	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠)))
22	15, 21	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠)))
23		psseq1 4053	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑡 → (𝑧 ⊊ 𝑠 ↔ 𝑡 ⊊ 𝑠))
24		treq 5222	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑡 → (Tr 𝑧 ↔ Tr 𝑡))
25	23, 24	anbi12d 632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑡 → ((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) ↔ (𝑡 ⊊ 𝑠 ∧ Tr 𝑡)))
26		elequ1 2116	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑡 → (𝑧 ∈ 𝑠 ↔ 𝑡 ∈ 𝑠))
27	25, 26	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑡 → (((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) ↔ ((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠)))
28	27	cbvalvw 2036	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) ↔ ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠))
29	22, 28	imbitrdi 251	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠)))
30	29	impcom 407	. . . . . . . . . . . . 13 ⊢ ((∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦)) → ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠))
31	30	ad2ant2l 746	. . . . . . . . . . . 12 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠))
32	31	adantr 480	. . . . . . . . . . 11 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠))
33		vex 3451	. . . . . . . . . . . . 13 ⊢ 𝑤 ∈ V
34		vex 3451	. . . . . . . . . . . . 13 ⊢ 𝑠 ∈ V
35	33, 34	dfon2lem5 35775	. . . . . . . . . . . 12 ⊢ ((∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤) ∧ ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠)) → (𝑤 ∈ 𝑠 ∨ 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤))
36		3orrot 1091	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ 𝑠 ∨ 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤) ↔ (𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠))
37		3orass 1089	. . . . . . . . . . . . . 14 ⊢ ((𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠) ↔ (𝑤 = 𝑠 ∨ (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)))
38	36, 37	bitri 275	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ 𝑠 ∨ 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤) ↔ (𝑤 = 𝑠 ∨ (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)))
39		eleq1a 2823	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 = 𝑠 → 𝑤 ∈ (𝑆 ∖ 𝑦)))
40		elndif 4096	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ 𝑦 → ¬ 𝑤 ∈ (𝑆 ∖ 𝑦))
41	39, 40	nsyli 157	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 ∈ 𝑦 → ¬ 𝑤 = 𝑠))
42	41	imp 406	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 ∈ (𝑆 ∖ 𝑦) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑤 = 𝑠)
43	42	adantll 714	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦)) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑤 = 𝑠)
44	43	adantll 714	. . . . . . . . . . . . . 14 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑤 = 𝑠)
45		orel1 888	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑤 = 𝑠 → ((𝑤 = 𝑠 ∨ (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)) → (𝑠 ∈ 𝑤 ∨ 𝑤 ∈ 𝑠)))
46		trss 5225	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Tr 𝑦 → (𝑤 ∈ 𝑦 → 𝑤 ⊆ 𝑦))
47		eldifn 4095	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → ¬ 𝑠 ∈ 𝑦)
48		ssel 3940	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ⊆ 𝑦 → (𝑠 ∈ 𝑤 → 𝑠 ∈ 𝑦))
49	48	con3d 152	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ⊆ 𝑦 → (¬ 𝑠 ∈ 𝑦 → ¬ 𝑠 ∈ 𝑤))
50	47, 49	syl5com 31	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 ⊆ 𝑦 → ¬ 𝑠 ∈ 𝑤))
51	46, 50	syl9 77	. . . . . . . . . . . . . . . . . . 19 ⊢ (Tr 𝑦 → (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 ∈ 𝑦 → ¬ 𝑠 ∈ 𝑤)))
52	51	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑤 ∈ 𝑦 → ¬ 𝑠 ∈ 𝑤)))
53	52	imp31 417	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦)) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑠 ∈ 𝑤)
54	53	adantll 714	. . . . . . . . . . . . . . . 16 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ¬ 𝑠 ∈ 𝑤)
55		orel1 888	. . . . . . . . . . . . . . . 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	biimtrid 242	. . . . . . . . . . . 12 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ((𝑤 ∈ 𝑠 ∨ 𝑤 = 𝑠 ∨ 𝑠 ∈ 𝑤) → 𝑤 ∈ 𝑠))
60	35, 59	syl5 34	. . . . . . . . . . 11 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → ((∀𝑧((𝑧 ⊊ 𝑤 ∧ Tr 𝑧) → 𝑧 ∈ 𝑤) ∧ ∀𝑡((𝑡 ⊊ 𝑠 ∧ Tr 𝑡) → 𝑡 ∈ 𝑠)) → 𝑤 ∈ 𝑠))
61	14, 32, 60	mp2and 699	. . . . . . . . . 10 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝑠)
62	61	ex 412	. . . . . . . . 9 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑠))
63	62	ssrdv 3952	. . . . . . . 8 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → 𝑦 ⊆ 𝑠)
64		dfpss2 4051	. . . . . . . . 9 ⊢ (𝑦 ⊊ 𝑠 ↔ (𝑦 ⊆ 𝑠 ∧ ¬ 𝑦 = 𝑠))
65		psseq1 4053	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑦 → (𝑧 ⊊ 𝑠 ↔ 𝑦 ⊊ 𝑠))
66		treq 5222	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑦 → (Tr 𝑧 ↔ Tr 𝑦))
67	65, 66	anbi12d 632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → ((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) ↔ (𝑦 ⊊ 𝑠 ∧ Tr 𝑦)))
68		elequ1 2116	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝑠 ↔ 𝑦 ∈ 𝑠))
69	67, 68	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑦 → (((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) ↔ ((𝑦 ⊊ 𝑠 ∧ Tr 𝑦) → 𝑦 ∈ 𝑠)))
70	69	spvv 1988	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑧((𝑧 ⊊ 𝑠 ∧ Tr 𝑧) → 𝑧 ∈ 𝑠) → ((𝑦 ⊊ 𝑠 ∧ Tr 𝑦) → 𝑦 ∈ 𝑠))
71	70	expd 415	. . . . . . . . . . . . . . 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 490	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥) → ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠))))
76	75	adantl 481	. . . . . . . . . 10 ⊢ ((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) → ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆 ∖ 𝑦) → (𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠))))
77	76	imp32 418	. . . . . . . . 9 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (𝑦 ⊊ 𝑠 → 𝑦 ∈ 𝑠))
78	64, 77	biimtrrid 243	. . . . . . . 8 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → ((𝑦 ⊆ 𝑠 ∧ ¬ 𝑦 = 𝑠) → 𝑦 ∈ 𝑠))
79	63, 78	mpand 695	. . . . . . 7 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (¬ 𝑦 = 𝑠 → 𝑦 ∈ 𝑠))
80	79	orrd 863	. . . . . 6 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦))) → (𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠))
81	80	anassrs 467	. . . . 5 ⊢ ((((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) ∧ 𝑠 ∈ (𝑆 ∖ 𝑦)) → (𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠))
82	81	ralrimiva 3125	. . . 4 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → ∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠))
83		pssdif 4332	. . . . . . 7 ⊢ (𝑦 ⊊ 𝑆 → (𝑆 ∖ 𝑦) ≠ ∅)
84		r19.2z 4458	. . . . . . . 8 ⊢ (((𝑆 ∖ 𝑦) ≠ ∅ ∧ ∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠)) → ∃𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠))
85	84	ex 412	. . . . . . 7 ⊢ ((𝑆 ∖ 𝑦) ≠ ∅ → (∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → ∃𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠)))
86	83, 85	syl 17	. . . . . 6 ⊢ (𝑦 ⊊ 𝑆 → (∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → ∃𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠)))
87	86	ad2antrl 728	. . . . 5 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (∀𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → ∃𝑠 ∈ (𝑆 ∖ 𝑦)(𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠)))
88		eleq1w 2811	. . . . . . . . . 10 ⊢ (𝑦 = 𝑠 → (𝑦 ∈ 𝑆 ↔ 𝑠 ∈ 𝑆))
89	15, 88	imbitrrid 246	. . . . . . . . 9 ⊢ (𝑦 = 𝑠 → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆))
90	89	a1i 11	. . . . . . . 8 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (𝑦 = 𝑠 → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆)))
91		trel 5223	. . . . . . . . . . 11 ⊢ (Tr 𝑆 → ((𝑦 ∈ 𝑠 ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ 𝑆))
92	91	expd 415	. . . . . . . . . 10 ⊢ (Tr 𝑆 → (𝑦 ∈ 𝑠 → (𝑠 ∈ 𝑆 → 𝑦 ∈ 𝑆)))
93	15, 92	syl7 74	. . . . . . . . 9 ⊢ (Tr 𝑆 → (𝑦 ∈ 𝑠 → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆)))
94	93	ad2antrr 726	. . . . . . . 8 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (𝑦 ∈ 𝑠 → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆)))
95	90, 94	jaod 859	. . . . . . 7 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → ((𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → (𝑠 ∈ (𝑆 ∖ 𝑦) → 𝑦 ∈ 𝑆)))
96	95	com23 86	. . . . . 6 ⊢ (((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) ∧ (𝑦 ⊊ 𝑆 ∧ Tr 𝑦)) → (𝑠 ∈ (𝑆 ∖ 𝑦) → ((𝑦 = 𝑠 ∨ 𝑦 ∈ 𝑠) → 𝑦 ∈ 𝑆)))
97	96	rexlimdv 3132	. . . . 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 412	. 2 ⊢ ((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) → ((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → 𝑦 ∈ 𝑆))
101	100	alrimiv 1927	1 ⊢ ((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) → ∀𝑦((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → 𝑦 ∈ 𝑆))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   ∨ w3o 1085  ∀wal 1538   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053   ∖ cdif 3911   ⊆ wss 3914   ⊊ wpss 3915  ∅c0 4296  Tr wtr 5214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-pw 4565  df-sn 4590  df-pr 4592  df-uni 4872  df-iun 4957  df-tr 5215  df-suc 6338

This theorem is referenced by:  dfon2lem7  35777  dfon2lem8  35778