Theorem dford3lem2

Description: Lemma for dford3 . (Contributed by Stefan O'Rear, 28-Oct-2014)

	Ref	Expression
Assertion	dford3lem2	⊢ ( ( Tr 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 Tr 𝑦 ) → 𝑥 ∈ On )

Proof

Step	Hyp	Ref	Expression
1		suctr	⊢ ( Tr 𝑥 → Tr suc 𝑥 )
2		vex	⊢ 𝑥 ∈ V
3	2	sucid	⊢ 𝑥 ∈ suc 𝑥
4	2	sucex	⊢ suc 𝑥 ∈ V
5		treq	⊢ ( 𝑐 = suc 𝑥 → ( Tr 𝑐 ↔ Tr suc 𝑥 ) )
6		eleq2	⊢ ( 𝑐 = suc 𝑥 → ( 𝑥 ∈ 𝑐 ↔ 𝑥 ∈ suc 𝑥 ) )
7	5 6	anbi12d	⊢ ( 𝑐 = suc 𝑥 → ( ( Tr 𝑐 ∧ 𝑥 ∈ 𝑐 ) ↔ ( Tr suc 𝑥 ∧ 𝑥 ∈ suc 𝑥 ) ) )
8	4 7	spcev	⊢ ( ( Tr suc 𝑥 ∧ 𝑥 ∈ suc 𝑥 ) → ∃ 𝑐 ( Tr 𝑐 ∧ 𝑥 ∈ 𝑐 ) )
9	1 3 8	sylancl	⊢ ( Tr 𝑥 → ∃ 𝑐 ( Tr 𝑐 ∧ 𝑥 ∈ 𝑐 ) )
10	9	adantr	⊢ ( ( Tr 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 Tr 𝑦 ) → ∃ 𝑐 ( Tr 𝑐 ∧ 𝑥 ∈ 𝑐 ) )
11		simprl	⊢ ( ( ∀ 𝑏 ∈ 𝑎 ( ( Tr 𝑏 ∧ ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) → 𝑏 ∈ On ) ∧ ( Tr 𝑎 ∧ ∀ 𝑦 ∈ 𝑎 Tr 𝑦 ) ) → Tr 𝑎 )
12		dford3lem1	⊢ ( ( Tr 𝑎 ∧ ∀ 𝑦 ∈ 𝑎 Tr 𝑦 ) → ∀ 𝑏 ∈ 𝑎 ( Tr 𝑏 ∧ ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) )
13		ralim	⊢ ( ∀ 𝑏 ∈ 𝑎 ( ( Tr 𝑏 ∧ ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) → 𝑏 ∈ On ) → ( ∀ 𝑏 ∈ 𝑎 ( Tr 𝑏 ∧ ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) → ∀ 𝑏 ∈ 𝑎 𝑏 ∈ On ) )
14	12 13	syl5	⊢ ( ∀ 𝑏 ∈ 𝑎 ( ( Tr 𝑏 ∧ ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) → 𝑏 ∈ On ) → ( ( Tr 𝑎 ∧ ∀ 𝑦 ∈ 𝑎 Tr 𝑦 ) → ∀ 𝑏 ∈ 𝑎 𝑏 ∈ On ) )
15	14	imp	⊢ ( ( ∀ 𝑏 ∈ 𝑎 ( ( Tr 𝑏 ∧ ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) → 𝑏 ∈ On ) ∧ ( Tr 𝑎 ∧ ∀ 𝑦 ∈ 𝑎 Tr 𝑦 ) ) → ∀ 𝑏 ∈ 𝑎 𝑏 ∈ On )
16		dfss3	⊢ ( 𝑎 ⊆ On ↔ ∀ 𝑏 ∈ 𝑎 𝑏 ∈ On )
17	15 16	sylibr	⊢ ( ( ∀ 𝑏 ∈ 𝑎 ( ( Tr 𝑏 ∧ ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) → 𝑏 ∈ On ) ∧ ( Tr 𝑎 ∧ ∀ 𝑦 ∈ 𝑎 Tr 𝑦 ) ) → 𝑎 ⊆ On )
18		ordon	⊢ Ord On
19	18	a1i	⊢ ( ( ∀ 𝑏 ∈ 𝑎 ( ( Tr 𝑏 ∧ ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) → 𝑏 ∈ On ) ∧ ( Tr 𝑎 ∧ ∀ 𝑦 ∈ 𝑎 Tr 𝑦 ) ) → Ord On )
20		trssord	⊢ ( ( Tr 𝑎 ∧ 𝑎 ⊆ On ∧ Ord On ) → Ord 𝑎 )
21	11 17 19 20	syl3anc	⊢ ( ( ∀ 𝑏 ∈ 𝑎 ( ( Tr 𝑏 ∧ ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) → 𝑏 ∈ On ) ∧ ( Tr 𝑎 ∧ ∀ 𝑦 ∈ 𝑎 Tr 𝑦 ) ) → Ord 𝑎 )
22		vex	⊢ 𝑎 ∈ V
23	22	elon	⊢ ( 𝑎 ∈ On ↔ Ord 𝑎 )
24	21 23	sylibr	⊢ ( ( ∀ 𝑏 ∈ 𝑎 ( ( Tr 𝑏 ∧ ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) → 𝑏 ∈ On ) ∧ ( Tr 𝑎 ∧ ∀ 𝑦 ∈ 𝑎 Tr 𝑦 ) ) → 𝑎 ∈ On )
25	24	ex	⊢ ( ∀ 𝑏 ∈ 𝑎 ( ( Tr 𝑏 ∧ ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) → 𝑏 ∈ On ) → ( ( Tr 𝑎 ∧ ∀ 𝑦 ∈ 𝑎 Tr 𝑦 ) → 𝑎 ∈ On ) )
26		treq	⊢ ( 𝑎 = 𝑏 → ( Tr 𝑎 ↔ Tr 𝑏 ) )
27		raleq	⊢ ( 𝑎 = 𝑏 → ( ∀ 𝑦 ∈ 𝑎 Tr 𝑦 ↔ ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) )
28	26 27	anbi12d	⊢ ( 𝑎 = 𝑏 → ( ( Tr 𝑎 ∧ ∀ 𝑦 ∈ 𝑎 Tr 𝑦 ) ↔ ( Tr 𝑏 ∧ ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) ) )
29		eleq1w	⊢ ( 𝑎 = 𝑏 → ( 𝑎 ∈ On ↔ 𝑏 ∈ On ) )
30	28 29	imbi12d	⊢ ( 𝑎 = 𝑏 → ( ( ( Tr 𝑎 ∧ ∀ 𝑦 ∈ 𝑎 Tr 𝑦 ) → 𝑎 ∈ On ) ↔ ( ( Tr 𝑏 ∧ ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) → 𝑏 ∈ On ) ) )
31		treq	⊢ ( 𝑎 = 𝑥 → ( Tr 𝑎 ↔ Tr 𝑥 ) )
32		raleq	⊢ ( 𝑎 = 𝑥 → ( ∀ 𝑦 ∈ 𝑎 Tr 𝑦 ↔ ∀ 𝑦 ∈ 𝑥 Tr 𝑦 ) )
33	31 32	anbi12d	⊢ ( 𝑎 = 𝑥 → ( ( Tr 𝑎 ∧ ∀ 𝑦 ∈ 𝑎 Tr 𝑦 ) ↔ ( Tr 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 Tr 𝑦 ) ) )
34		eleq1w	⊢ ( 𝑎 = 𝑥 → ( 𝑎 ∈ On ↔ 𝑥 ∈ On ) )
35	33 34	imbi12d	⊢ ( 𝑎 = 𝑥 → ( ( ( Tr 𝑎 ∧ ∀ 𝑦 ∈ 𝑎 Tr 𝑦 ) → 𝑎 ∈ On ) ↔ ( ( Tr 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 Tr 𝑦 ) → 𝑥 ∈ On ) ) )
36	25 30 35	setindtrs	⊢ ( ∃ 𝑐 ( Tr 𝑐 ∧ 𝑥 ∈ 𝑐 ) → ( ( Tr 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 Tr 𝑦 ) → 𝑥 ∈ On ) )
37	10 36	mpcom	⊢ ( ( Tr 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 Tr 𝑦 ) → 𝑥 ∈ On )