Theorem dfon2lem8 35771

Description: Lemma for dfon2 35773. 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 3481	. . . . . . 7 ⊢ 𝑥 ∈ V
2		dfon2lem3 35766	. . . . . . 7 ⊢ (𝑥 ∈ V → (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (Tr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧)))
3	1, 2	ax-mp 5	. . . . . 6 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (Tr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧))
4	3	simpld 494	. . . . 5 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → Tr 𝑥)
5	4	ralimi 3080	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑥 ∈ 𝐴 Tr 𝑥)
6		trint 5282	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∩ 𝐴)
7	5, 6	syl 17	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → Tr ∩ 𝐴)
8	7	adantl 481	. 2 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → Tr ∩ 𝐴)
9	1	dfon2lem7 35770	. . . . . . 7 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
10	9	alrimiv 1924	. . . . . 6 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
11	10	ralimi 3080	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑥 ∈ 𝐴 ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
12		df-ral 3059	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
13		19.21v 1936	. . . . . . . 8 ⊢ (∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) ↔ (𝑥 ∈ 𝐴 → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
14	13	albii 1815	. . . . . . 7 ⊢ (∀𝑥∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
15	12, 14	bitr4i 278	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑥∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
16		impexp 450	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ (𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
17	16	2albii 1816	. . . . . . 7 ⊢ (∀𝑥∀𝑤((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑥∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
18		eluni2 4915	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ∪ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥)
19	18	biimpi 216	. . . . . . . . . 10 ⊢ (𝑤 ∈ ∪ 𝐴 → ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥)
20	19	imim1i 63	. . . . . . . . 9 ⊢ ((∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → (𝑤 ∈ ∪ 𝐴 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
21	20	alimi 1807	. . . . . . . 8 ⊢ (∀𝑤(∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → ∀𝑤(𝑤 ∈ ∪ 𝐴 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
22		alcom 2156	. . . . . . . . 9 ⊢ (∀𝑥∀𝑤((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑤∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
23		19.23v 1939	. . . . . . . . . . 11 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
24		df-rex 3068	. . . . . . . . . . . 12 ⊢ (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥))
25	24	imbi1i 349	. . . . . . . . . . 11 ⊢ ((∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
26	23, 25	bitr4i 278	. . . . . . . . . 10 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
27	26	albii 1815	. . . . . . . . 9 ⊢ (∀𝑤∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
28	22, 27	bitri 275	. . . . . . . 8 ⊢ (∀𝑥∀𝑤((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
29		df-ral 3059	. . . . . . . 8 ⊢ (∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤) ↔ ∀𝑤(𝑤 ∈ ∪ 𝐴 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
30	21, 28, 29	3imtr4i 292	. . . . . . 7 ⊢ (∀𝑥∀𝑤((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → ∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))
31	17, 30	sylbir 235	. . . . . 6 ⊢ (∀𝑥∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) → ∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))
32	15, 31	sylbi 217	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → ∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))
33	11, 32	syl 17	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))
34	33	adantl 481	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → ∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))
35		intssuni 4974	. . . . 5 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴)
36		ssralv 4063	. . . . 5 ⊢ (∩ 𝐴 ⊆ ∪ 𝐴 → (∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤) → ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
37	35, 36	syl 17	. . . 4 ⊢ (𝐴 ≠ ∅ → (∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤) → ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
38	37	adantr 480	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤) → ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
39	34, 38	mpd 15	. 2 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))
40		dfon2lem6 35769	. . 3 ⊢ ((Tr ∩ 𝐴 ∧ ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴))
41		intex 5349	. . . . . . . . . . 11 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)
42		dfon2lem3 35766	. . . . . . . . . . 11 ⊢ (∩ 𝐴 ∈ V → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) → (Tr ∩ 𝐴 ∧ ∀𝑡 ∈ ∩ 𝐴 ¬ 𝑡 ∈ 𝑡)))
43	41, 42	sylbi 217	. . . . . . . . . 10 ⊢ (𝐴 ≠ ∅ → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) → (Tr ∩ 𝐴 ∧ ∀𝑡 ∈ ∩ 𝐴 ¬ 𝑡 ∈ 𝑡)))
44	43	imp 406	. . . . . . . . 9 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (Tr ∩ 𝐴 ∧ ∀𝑡 ∈ ∩ 𝐴 ¬ 𝑡 ∈ 𝑡))
45	44	simprd 495	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → ∀𝑡 ∈ ∩ 𝐴 ¬ 𝑡 ∈ 𝑡)
46		untelirr 35687	. . . . . . . 8 ⊢ (∀𝑡 ∈ ∩ 𝐴 ¬ 𝑡 ∈ 𝑡 → ¬ ∩ 𝐴 ∈ ∩ 𝐴)
47	45, 46	syl 17	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → ¬ ∩ 𝐴 ∈ ∩ 𝐴)
48	47	adantlr 715	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → ¬ ∩ 𝐴 ∈ ∩ 𝐴)
49		risset 3230	. . . . . . . . . 10 ⊢ (∩ 𝐴 ∈ 𝐴 ↔ ∃𝑡 ∈ 𝐴 𝑡 = ∩ 𝐴)
50	49	notbii 320	. . . . . . . . 9 ⊢ (¬ ∩ 𝐴 ∈ 𝐴 ↔ ¬ ∃𝑡 ∈ 𝐴 𝑡 = ∩ 𝐴)
51		ralnex 3069	. . . . . . . . 9 ⊢ (∀𝑡 ∈ 𝐴 ¬ 𝑡 = ∩ 𝐴 ↔ ¬ ∃𝑡 ∈ 𝐴 𝑡 = ∩ 𝐴)
52	50, 51	bitr4i 278	. . . . . . . 8 ⊢ (¬ ∩ 𝐴 ∈ 𝐴 ↔ ∀𝑡 ∈ 𝐴 ¬ 𝑡 = ∩ 𝐴)
53		eqcom 2741	. . . . . . . . . . . 12 ⊢ (𝑡 = ∩ 𝐴 ↔ ∩ 𝐴 = 𝑡)
54	53	notbii 320	. . . . . . . . . . 11 ⊢ (¬ 𝑡 = ∩ 𝐴 ↔ ¬ ∩ 𝐴 = 𝑡)
55	44	simpld 494	. . . . . . . . . . . . 13 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → Tr ∩ 𝐴)
56	55	adantlr 715	. . . . . . . . . . . 12 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → Tr ∩ 𝐴)
57		psseq2 4100	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑡 → (𝑦 ⊊ 𝑥 ↔ 𝑦 ⊊ 𝑡))
58	57	anbi1d 631	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑡 → ((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) ↔ (𝑦 ⊊ 𝑡 ∧ Tr 𝑦)))
59		elequ2 2120	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑡 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑡))
60	58, 59	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑡 → (((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) ↔ ((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)))
61	60	albidv 1917	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑡 → (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) ↔ ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)))
62	61	rspccv 3618	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (𝑡 ∈ 𝐴 → ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)))
63	62	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (𝑡 ∈ 𝐴 → ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)))
64		intss1 4967	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑡)
65		dfpss2 4097	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∩ 𝐴 ⊊ 𝑡 ↔ (∩ 𝐴 ⊆ 𝑡 ∧ ¬ ∩ 𝐴 = 𝑡))
66		psseq1 4099	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = ∩ 𝐴 → (𝑦 ⊊ 𝑡 ↔ ∩ 𝐴 ⊊ 𝑡))
67		treq 5272	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = ∩ 𝐴 → (Tr 𝑦 ↔ Tr ∩ 𝐴))
68	66, 67	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ∩ 𝐴 → ((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) ↔ (∩ 𝐴 ⊊ 𝑡 ∧ Tr ∩ 𝐴)))
69		eleq1 2826	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ∩ 𝐴 → (𝑦 ∈ 𝑡 ↔ ∩ 𝐴 ∈ 𝑡))
70	68, 69	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ∩ 𝐴 → (((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) ↔ ((∩ 𝐴 ⊊ 𝑡 ∧ Tr ∩ 𝐴) → ∩ 𝐴 ∈ 𝑡)))
71	70	spcgv 3595	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∩ 𝐴 ∈ V → (∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → ((∩ 𝐴 ⊊ 𝑡 ∧ Tr ∩ 𝐴) → ∩ 𝐴 ∈ 𝑡)))
72	41, 71	sylbi 217	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ≠ ∅ → (∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → ((∩ 𝐴 ⊊ 𝑡 ∧ Tr ∩ 𝐴) → ∩ 𝐴 ∈ 𝑡)))
73	72	imp 406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)) → ((∩ 𝐴 ⊊ 𝑡 ∧ Tr ∩ 𝐴) → ∩ 𝐴 ∈ 𝑡))
74	73	expd 415	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)) → (∩ 𝐴 ⊊ 𝑡 → (Tr ∩ 𝐴 → ∩ 𝐴 ∈ 𝑡)))
75	65, 74	biimtrrid 243	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)) → ((∩ 𝐴 ⊆ 𝑡 ∧ ¬ ∩ 𝐴 = 𝑡) → (Tr ∩ 𝐴 → ∩ 𝐴 ∈ 𝑡)))
76	75	exp4b 430	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ≠ ∅ → (∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → (∩ 𝐴 ⊆ 𝑡 → (¬ ∩ 𝐴 = 𝑡 → (Tr ∩ 𝐴 → ∩ 𝐴 ∈ 𝑡)))))
77	76	com45 97	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ≠ ∅ → (∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → (∩ 𝐴 ⊆ 𝑡 → (Tr ∩ 𝐴 → (¬ ∩ 𝐴 = 𝑡 → ∩ 𝐴 ∈ 𝑡)))))
78	77	com23 86	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ≠ ∅ → (∩ 𝐴 ⊆ 𝑡 → (∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → (Tr ∩ 𝐴 → (¬ ∩ 𝐴 = 𝑡 → ∩ 𝐴 ∈ 𝑡)))))
79	64, 78	syl5 34	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ≠ ∅ → (𝑡 ∈ 𝐴 → (∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → (Tr ∩ 𝐴 → (¬ ∩ 𝐴 = 𝑡 → ∩ 𝐴 ∈ 𝑡)))))
80	79	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (𝑡 ∈ 𝐴 → (∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → (Tr ∩ 𝐴 → (¬ ∩ 𝐴 = 𝑡 → ∩ 𝐴 ∈ 𝑡)))))
81	63, 80	mpdd 43	. . . . . . . . . . . . 13 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (𝑡 ∈ 𝐴 → (Tr ∩ 𝐴 → (¬ ∩ 𝐴 = 𝑡 → ∩ 𝐴 ∈ 𝑡))))
82	81	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (𝑡 ∈ 𝐴 → (Tr ∩ 𝐴 → (¬ ∩ 𝐴 = 𝑡 → ∩ 𝐴 ∈ 𝑡))))
83	56, 82	mpid 44	. . . . . . . . . . 11 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (𝑡 ∈ 𝐴 → (¬ ∩ 𝐴 = 𝑡 → ∩ 𝐴 ∈ 𝑡)))
84	54, 83	syl7bi 255	. . . . . . . . . 10 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (𝑡 ∈ 𝐴 → (¬ 𝑡 = ∩ 𝐴 → ∩ 𝐴 ∈ 𝑡)))
85	84	ralrimiv 3142	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → ∀𝑡 ∈ 𝐴 (¬ 𝑡 = ∩ 𝐴 → ∩ 𝐴 ∈ 𝑡))
86		ralim 3083	. . . . . . . . 9 ⊢ (∀𝑡 ∈ 𝐴 (¬ 𝑡 = ∩ 𝐴 → ∩ 𝐴 ∈ 𝑡) → (∀𝑡 ∈ 𝐴 ¬ 𝑡 = ∩ 𝐴 → ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡))
87	85, 86	syl 17	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (∀𝑡 ∈ 𝐴 ¬ 𝑡 = ∩ 𝐴 → ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡))
88	52, 87	biimtrid 242	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (¬ ∩ 𝐴 ∈ 𝐴 → ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡))
89		elintg 4958	. . . . . . . . 9 ⊢ (∩ 𝐴 ∈ V → (∩ 𝐴 ∈ ∩ 𝐴 ↔ ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡))
90	41, 89	sylbi 217	. . . . . . . 8 ⊢ (𝐴 ≠ ∅ → (∩ 𝐴 ∈ ∩ 𝐴 ↔ ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡))
91	90	ad2antrr 726	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (∩ 𝐴 ∈ ∩ 𝐴 ↔ ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡))
92	88, 91	sylibrd 259	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (¬ ∩ 𝐴 ∈ 𝐴 → ∩ 𝐴 ∈ ∩ 𝐴))
93	48, 92	mt3d 148	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → ∩ 𝐴 ∈ 𝐴)
94	93	ex 412	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) → ∩ 𝐴 ∈ 𝐴))
95	94	ancld 550	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) ∧ ∩ 𝐴 ∈ 𝐴)))
96	40, 95	syl5 34	. 2 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → ((Tr ∩ 𝐴 ∧ ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) ∧ ∩ 𝐴 ∈ 𝐴)))
97	8, 39, 96	mp2and 699	1 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) ∧ ∩ 𝐴 ∈ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1534   = wceq 1536  ∃wex 1775   ∈ wcel 2105   ≠ wne 2937  ∀wral 3058  ∃wrex 3067  Vcvv 3477   ⊆ wss 3962   ⊊ wpss 3963  ∅c0 4338  ∪ cuni 4911  ∩ cint 4950  Tr wtr 5264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-pw 4606  df-sn 4631  df-pr 4633  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-tr 5265  df-suc 6391

This theorem is referenced by:  dfon2lem9  35772