Theorem dfon2lem8 36319

Description: Lemma for dfon2 36321. The intersection of a nonempty class 𝐴 of new ordinals is itself a new ordinal and is contained within 𝐴 (Contributed by Scott Fenton, 26-Feb-2011.)

Assertion

Ref	Expression
dfon2lem8	⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) ∧ ∩ 𝐴 ∈ 𝐴))

Distinct variable group:   𝑥,𝐴,𝑦,𝑧

Proof of Theorem dfon2lem8

Dummy variables 𝑤 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3461	. . . . . . 7 ⊢ 𝑥 ∈ V
2		dfon2lem3 36314	. . . . . . 7 ⊢ (𝑥 ∈ V → (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (Tr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧)))
3	1, 2	ax-mp 5	. . . . . 6 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (Tr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧))
4	3	simpld 500	. . . . 5 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → Tr 𝑥)
5	4	ralimi 3104	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑥 ∈ 𝐴 Tr 𝑥)
6		trint 5238	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∩ 𝐴)
7	5, 6	syl 18	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → Tr ∩ 𝐴)
8	7	adantl 487	. 2 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → Tr ∩ 𝐴)
9	1	dfon2lem7 36318	. . . . . . 7 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
10	9	alrimiv 1960	. . . . . 6 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
11	10	ralimi 3104	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑥 ∈ 𝐴 ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
12		df-ral 3082	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
13		19.21v 1972	. . . . . . . 8 ⊢ (∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) ↔ (𝑥 ∈ 𝐴 → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
14	13	albii 1852	. . . . . . 7 ⊢ (∀𝑥∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
15	12, 14	bitr4i 281	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑥∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
16		impexp 456	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ (𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
17	16	2albii 1853	. . . . . . 7 ⊢ (∀𝑥∀𝑤((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑥∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
18		eluni2 4878	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ∪ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥)
19	18	biimpi 219	. . . . . . . . . 10 ⊢ (𝑤 ∈ ∪ 𝐴 → ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥)
20	19	imim1i 64	. . . . . . . . 9 ⊢ ((∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → (𝑤 ∈ ∪ 𝐴 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
21	20	alimi 1844	. . . . . . . 8 ⊢ (∀𝑤(∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → ∀𝑤(𝑤 ∈ ∪ 𝐴 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
22		alcom 2197	. . . . . . . . 9 ⊢ (∀𝑥∀𝑤((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑤∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
23		19.23v 1975	. . . . . . . . . . 11 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
24		df-rex 3092	. . . . . . . . . . . 12 ⊢ (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥))
25	24	imbi1i 352	. . . . . . . . . . 11 ⊢ ((∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
26	23, 25	bitr4i 281	. . . . . . . . . 10 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
27	26	albii 1852	. . . . . . . . 9 ⊢ (∀𝑤∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
28	22, 27	bitri 278	. . . . . . . 8 ⊢ (∀𝑥∀𝑤((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
29		df-ral 3082	. . . . . . . 8 ⊢ (∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤) ↔ ∀𝑤(𝑤 ∈ ∪ 𝐴 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
30	21, 28, 29	3imtr4i 295	. . . . . . 7 ⊢ (∀𝑥∀𝑤((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → ∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))
31	17, 30	sylbir 238	. . . . . 6 ⊢ (∀𝑥∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) → ∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))
32	15, 31	sylbi 220	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → ∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))
33	11, 32	syl 18	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))
34	33	adantl 487	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → ∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))
35		intssuni 4937	. . . . 5 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴)
36		ssralv 4007	. . . . 5 ⊢ (∩ 𝐴 ⊆ ∪ 𝐴 → (∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤) → ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
37	35, 36	syl 18	. . . 4 ⊢ (𝐴 ≠ ∅ → (∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤) → ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
38	37	adantr 486	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤) → ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
39	34, 38	mpd 16	. 2 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))
40		dfon2lem6 36317	. . 3 ⊢ ((Tr ∩ 𝐴 ∧ ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴))
41		intex 5316	. . . . . . . . . . 11 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)
42		dfon2lem3 36314	. . . . . . . . . . 11 ⊢ (∩ 𝐴 ∈ V → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) → (Tr ∩ 𝐴 ∧ ∀𝑡 ∈ ∩ 𝐴 ¬ 𝑡 ∈ 𝑡)))
43	41, 42	sylbi 220	. . . . . . . . . 10 ⊢ (𝐴 ≠ ∅ → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) → (Tr ∩ 𝐴 ∧ ∀𝑡 ∈ ∩ 𝐴 ¬ 𝑡 ∈ 𝑡)))
44	43	imp 412	. . . . . . . . 9 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (Tr ∩ 𝐴 ∧ ∀𝑡 ∈ ∩ 𝐴 ¬ 𝑡 ∈ 𝑡))
45	44	simprd 501	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → ∀𝑡 ∈ ∩ 𝐴 ¬ 𝑡 ∈ 𝑡)
46		untelirr 36239	. . . . . . . 8 ⊢ (∀𝑡 ∈ ∩ 𝐴 ¬ 𝑡 ∈ 𝑡 → ¬ ∩ 𝐴 ∈ ∩ 𝐴)
47	45, 46	syl 18	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → ¬ ∩ 𝐴 ∈ ∩ 𝐴)
48	47	adantlr 728	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → ¬ ∩ 𝐴 ∈ ∩ 𝐴)
49		risset 3242	. . . . . . . . . 10 ⊢ (∩ 𝐴 ∈ 𝐴 ↔ ∃𝑡 ∈ 𝐴 𝑡 = ∩ 𝐴)
50	49	notbii 323	. . . . . . . . 9 ⊢ (¬ ∩ 𝐴 ∈ 𝐴 ↔ ¬ ∃𝑡 ∈ 𝐴 𝑡 = ∩ 𝐴)
51		ralnex 3093	. . . . . . . . 9 ⊢ (∀𝑡 ∈ 𝐴 ¬ 𝑡 = ∩ 𝐴 ↔ ¬ ∃𝑡 ∈ 𝐴 𝑡 = ∩ 𝐴)
52	50, 51	bitr4i 281	. . . . . . . 8 ⊢ (¬ ∩ 𝐴 ∈ 𝐴 ↔ ∀𝑡 ∈ 𝐴 ¬ 𝑡 = ∩ 𝐴)
53		eqcom 2772	. . . . . . . . . . . 12 ⊢ (𝑡 = ∩ 𝐴 ↔ ∩ 𝐴 = 𝑡)
54	53	notbii 323	. . . . . . . . . . 11 ⊢ (¬ 𝑡 = ∩ 𝐴 ↔ ¬ ∩ 𝐴 = 𝑡)
55	44	simpld 500	. . . . . . . . . . . . 13 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → Tr ∩ 𝐴)
56	55	adantlr 728	. . . . . . . . . . . 12 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → Tr ∩ 𝐴)
57		psseq2 4046	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑡 → (𝑦 ⊊ 𝑥 ↔ 𝑦 ⊊ 𝑡))
58	57	anbi1d 643	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑡 → ((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) ↔ (𝑦 ⊊ 𝑡 ∧ Tr 𝑦)))
59		elequ2 2161	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑡 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑡))
60	58, 59	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑡 → (((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) ↔ ((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)))
61	60	albidv 1953	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑡 → (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) ↔ ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)))
62	61	rspccv 3580	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (𝑡 ∈ 𝐴 → ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)))
63	62	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (𝑡 ∈ 𝐴 → ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)))
64		intss1 4930	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑡)
65		dfpss2 4043	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∩ 𝐴 ⊊ 𝑡 ↔ (∩ 𝐴 ⊆ 𝑡 ∧ ¬ ∩ 𝐴 = 𝑡))
66		psseq1 4045	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = ∩ 𝐴 → (𝑦 ⊊ 𝑡 ↔ ∩ 𝐴 ⊊ 𝑡))
67		treq 5227	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = ∩ 𝐴 → (Tr 𝑦 ↔ Tr ∩ 𝐴))
68	66, 67	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ∩ 𝐴 → ((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) ↔ (∩ 𝐴 ⊊ 𝑡 ∧ Tr ∩ 𝐴)))
69		eleq1 2853	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ∩ 𝐴 → (𝑦 ∈ 𝑡 ↔ ∩ 𝐴 ∈ 𝑡))
70	68, 69	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ∩ 𝐴 → (((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) ↔ ((∩ 𝐴 ⊊ 𝑡 ∧ Tr ∩ 𝐴) → ∩ 𝐴 ∈ 𝑡)))
71	70	spcgv 3557	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∩ 𝐴 ∈ V → (∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → ((∩ 𝐴 ⊊ 𝑡 ∧ Tr ∩ 𝐴) → ∩ 𝐴 ∈ 𝑡)))
72	41, 71	sylbi 220	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ≠ ∅ → (∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → ((∩ 𝐴 ⊊ 𝑡 ∧ Tr ∩ 𝐴) → ∩ 𝐴 ∈ 𝑡)))
73	72	imp 412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)) → ((∩ 𝐴 ⊊ 𝑡 ∧ Tr ∩ 𝐴) → ∩ 𝐴 ∈ 𝑡))
74	73	expd 421	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)) → (∩ 𝐴 ⊊ 𝑡 → (Tr ∩ 𝐴 → ∩ 𝐴 ∈ 𝑡)))
75	65, 74	biimtrrid 246	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)) → ((∩ 𝐴 ⊆ 𝑡 ∧ ¬ ∩ 𝐴 = 𝑡) → (Tr ∩ 𝐴 → ∩ 𝐴 ∈ 𝑡)))
76	75	exp4b 436	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ≠ ∅ → (∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → (∩ 𝐴 ⊆ 𝑡 → (¬ ∩ 𝐴 = 𝑡 → (Tr ∩ 𝐴 → ∩ 𝐴 ∈ 𝑡)))))
77	76	com45 98	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ≠ ∅ → (∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → (∩ 𝐴 ⊆ 𝑡 → (Tr ∩ 𝐴 → (¬ ∩ 𝐴 = 𝑡 → ∩ 𝐴 ∈ 𝑡)))))
78	77	com23 87	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ≠ ∅ → (∩ 𝐴 ⊆ 𝑡 → (∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → (Tr ∩ 𝐴 → (¬ ∩ 𝐴 = 𝑡 → ∩ 𝐴 ∈ 𝑡)))))
79	64, 78	syl5 35	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ≠ ∅ → (𝑡 ∈ 𝐴 → (∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → (Tr ∩ 𝐴 → (¬ ∩ 𝐴 = 𝑡 → ∩ 𝐴 ∈ 𝑡)))))
80	79	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (𝑡 ∈ 𝐴 → (∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → (Tr ∩ 𝐴 → (¬ ∩ 𝐴 = 𝑡 → ∩ 𝐴 ∈ 𝑡)))))
81	63, 80	mpdd 44	. . . . . . . . . . . . 13 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (𝑡 ∈ 𝐴 → (Tr ∩ 𝐴 → (¬ ∩ 𝐴 = 𝑡 → ∩ 𝐴 ∈ 𝑡))))
82	81	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (𝑡 ∈ 𝐴 → (Tr ∩ 𝐴 → (¬ ∩ 𝐴 = 𝑡 → ∩ 𝐴 ∈ 𝑡))))
83	56, 82	mpid 45	. . . . . . . . . . 11 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (𝑡 ∈ 𝐴 → (¬ ∩ 𝐴 = 𝑡 → ∩ 𝐴 ∈ 𝑡)))
84	54, 83	syl7bi 258	. . . . . . . . . 10 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (𝑡 ∈ 𝐴 → (¬ 𝑡 = ∩ 𝐴 → ∩ 𝐴 ∈ 𝑡)))
85	84	ralrimiv 3158	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → ∀𝑡 ∈ 𝐴 (¬ 𝑡 = ∩ 𝐴 → ∩ 𝐴 ∈ 𝑡))
86		ralim 3107	. . . . . . . . 9 ⊢ (∀𝑡 ∈ 𝐴 (¬ 𝑡 = ∩ 𝐴 → ∩ 𝐴 ∈ 𝑡) → (∀𝑡 ∈ 𝐴 ¬ 𝑡 = ∩ 𝐴 → ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡))
87	85, 86	syl 18	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (∀𝑡 ∈ 𝐴 ¬ 𝑡 = ∩ 𝐴 → ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡))
88	52, 87	biimtrid 245	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (¬ ∩ 𝐴 ∈ 𝐴 → ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡))
89		elintg 4922	. . . . . . . . 9 ⊢ (∩ 𝐴 ∈ V → (∩ 𝐴 ∈ ∩ 𝐴 ↔ ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡))
90	41, 89	sylbi 220	. . . . . . . 8 ⊢ (𝐴 ≠ ∅ → (∩ 𝐴 ∈ ∩ 𝐴 ↔ ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡))
91	90	ad2antrr 739	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (∩ 𝐴 ∈ ∩ 𝐴 ↔ ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡))
92	88, 91	sylibrd 262	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (¬ ∩ 𝐴 ∈ 𝐴 → ∩ 𝐴 ∈ ∩ 𝐴))
93	48, 92	mt3d 149	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → ∩ 𝐴 ∈ 𝐴)
94	93	ex 418	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) → ∩ 𝐴 ∈ 𝐴))
95	94	ancld 560	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) ∧ ∩ 𝐴 ∈ 𝐴)))
96	40, 95	syl5 35	. 2 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → ((Tr ∩ 𝐴 ∧ ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) ∧ ∩ 𝐴 ∈ 𝐴)))
97	8, 39, 96	mp2and 712	1 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) ∧ ∩ 𝐴 ∈ 𝐴))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2146   ≠ wne 2960  ∀wral 3081  ∃wrex 3091  Vcvv 3457   ⊆ wss 3906   ⊊ wpss 3907  ∅c0 4286  ∪ cuni 4874  ∩ cint 4914  Tr wtr 5220

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-pr 5406  ax-un 7742

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 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-pw 4566  df-sn 4592  df-pr 4594  df-uni 4875  df-int 4915  df-iun 4960  df-iin 4961  df-tr 5221  df-suc 6370

This theorem is used by:  dfon2lem9  36320