Theorem dfon2lem8 33030

Description: Lemma for dfon2 33032. 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 3498	. . . . . . 7 ⊢ 𝑥 ∈ V
2		dfon2lem3 33025	. . . . . . 7 ⊢ (𝑥 ∈ V → (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (Tr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧)))
3	1, 2	ax-mp 5	. . . . . 6 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (Tr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧))
4	3	simpld 497	. . . . 5 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → Tr 𝑥)
5	4	ralimi 3160	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑥 ∈ 𝐴 Tr 𝑥)
6		trint 5181	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∩ 𝐴)
7	5, 6	syl 17	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → Tr ∩ 𝐴)
8	7	adantl 484	. 2 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → Tr ∩ 𝐴)
9	1	dfon2lem7 33029	. . . . . . 7 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
10	9	alrimiv 1924	. . . . . 6 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
11	10	ralimi 3160	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑥 ∈ 𝐴 ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
12		df-ral 3143	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
13		19.21v 1936	. . . . . . . 8 ⊢ (∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) ↔ (𝑥 ∈ 𝐴 → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
14	13	albii 1816	. . . . . . 7 ⊢ (∀𝑥∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
15	12, 14	bitr4i 280	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑥∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
16		impexp 453	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ (𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
17	16	2albii 1817	. . . . . . 7 ⊢ (∀𝑥∀𝑤((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑥∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
18		eluni2 4836	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ∪ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥)
19	18	biimpi 218	. . . . . . . . . 10 ⊢ (𝑤 ∈ ∪ 𝐴 → ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥)
20	19	imim1i 63	. . . . . . . . 9 ⊢ ((∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → (𝑤 ∈ ∪ 𝐴 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
21	20	alimi 1808	. . . . . . . 8 ⊢ (∀𝑤(∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → ∀𝑤(𝑤 ∈ ∪ 𝐴 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
22		alcom 2158	. . . . . . . . 9 ⊢ (∀𝑥∀𝑤((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑤∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
23		19.23v 1939	. . . . . . . . . . 11 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
24		df-rex 3144	. . . . . . . . . . . 12 ⊢ (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥))
25	24	imbi1i 352	. . . . . . . . . . 11 ⊢ ((∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
26	23, 25	bitr4i 280	. . . . . . . . . 10 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
27	26	albii 1816	. . . . . . . . 9 ⊢ (∀𝑤∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
28	22, 27	bitri 277	. . . . . . . 8 ⊢ (∀𝑥∀𝑤((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
29		df-ral 3143	. . . . . . . 8 ⊢ (∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤) ↔ ∀𝑤(𝑤 ∈ ∪ 𝐴 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
30	21, 28, 29	3imtr4i 294	. . . . . . 7 ⊢ (∀𝑥∀𝑤((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → ∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))
31	17, 30	sylbir 237	. . . . . 6 ⊢ (∀𝑥∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) → ∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))
32	15, 31	sylbi 219	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → ∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))
33	11, 32	syl 17	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))
34	33	adantl 484	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → ∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))
35		intssuni 4891	. . . . 5 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴)
36		ssralv 4033	. . . . 5 ⊢ (∩ 𝐴 ⊆ ∪ 𝐴 → (∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤) → ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
37	35, 36	syl 17	. . . 4 ⊢ (𝐴 ≠ ∅ → (∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤) → ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
38	37	adantr 483	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤) → ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
39	34, 38	mpd 15	. 2 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))
40		dfon2lem6 33028	. . 3 ⊢ ((Tr ∩ 𝐴 ∧ ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴))
41		intex 5233	. . . . . . . . . . 11 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)
42		dfon2lem3 33025	. . . . . . . . . . 11 ⊢ (∩ 𝐴 ∈ V → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) → (Tr ∩ 𝐴 ∧ ∀𝑡 ∈ ∩ 𝐴 ¬ 𝑡 ∈ 𝑡)))
43	41, 42	sylbi 219	. . . . . . . . . 10 ⊢ (𝐴 ≠ ∅ → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) → (Tr ∩ 𝐴 ∧ ∀𝑡 ∈ ∩ 𝐴 ¬ 𝑡 ∈ 𝑡)))
44	43	imp 409	. . . . . . . . 9 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (Tr ∩ 𝐴 ∧ ∀𝑡 ∈ ∩ 𝐴 ¬ 𝑡 ∈ 𝑡))
45	44	simprd 498	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → ∀𝑡 ∈ ∩ 𝐴 ¬ 𝑡 ∈ 𝑡)
46		untelirr 32929	. . . . . . . 8 ⊢ (∀𝑡 ∈ ∩ 𝐴 ¬ 𝑡 ∈ 𝑡 → ¬ ∩ 𝐴 ∈ ∩ 𝐴)
47	45, 46	syl 17	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → ¬ ∩ 𝐴 ∈ ∩ 𝐴)
48	47	adantlr 713	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → ¬ ∩ 𝐴 ∈ ∩ 𝐴)
49		risset 3267	. . . . . . . . . 10 ⊢ (∩ 𝐴 ∈ 𝐴 ↔ ∃𝑡 ∈ 𝐴 𝑡 = ∩ 𝐴)
50	49	notbii 322	. . . . . . . . 9 ⊢ (¬ ∩ 𝐴 ∈ 𝐴 ↔ ¬ ∃𝑡 ∈ 𝐴 𝑡 = ∩ 𝐴)
51		ralnex 3236	. . . . . . . . 9 ⊢ (∀𝑡 ∈ 𝐴 ¬ 𝑡 = ∩ 𝐴 ↔ ¬ ∃𝑡 ∈ 𝐴 𝑡 = ∩ 𝐴)
52	50, 51	bitr4i 280	. . . . . . . 8 ⊢ (¬ ∩ 𝐴 ∈ 𝐴 ↔ ∀𝑡 ∈ 𝐴 ¬ 𝑡 = ∩ 𝐴)
53		eqcom 2828	. . . . . . . . . . . 12 ⊢ (𝑡 = ∩ 𝐴 ↔ ∩ 𝐴 = 𝑡)
54	53	notbii 322	. . . . . . . . . . 11 ⊢ (¬ 𝑡 = ∩ 𝐴 ↔ ¬ ∩ 𝐴 = 𝑡)
55	44	simpld 497	. . . . . . . . . . . . 13 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → Tr ∩ 𝐴)
56	55	adantlr 713	. . . . . . . . . . . 12 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → Tr ∩ 𝐴)
57		psseq2 4065	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑡 → (𝑦 ⊊ 𝑥 ↔ 𝑦 ⊊ 𝑡))
58	57	anbi1d 631	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑡 → ((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) ↔ (𝑦 ⊊ 𝑡 ∧ Tr 𝑦)))
59		elequ2 2125	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑡 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑡))
60	58, 59	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑡 → (((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) ↔ ((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)))
61	60	albidv 1917	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑡 → (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) ↔ ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)))
62	61	rspccv 3620	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (𝑡 ∈ 𝐴 → ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)))
63	62	adantl 484	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (𝑡 ∈ 𝐴 → ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)))
64		intss1 4884	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑡)
65		dfpss2 4062	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∩ 𝐴 ⊊ 𝑡 ↔ (∩ 𝐴 ⊆ 𝑡 ∧ ¬ ∩ 𝐴 = 𝑡))
66		psseq1 4064	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = ∩ 𝐴 → (𝑦 ⊊ 𝑡 ↔ ∩ 𝐴 ⊊ 𝑡))
67		treq 5171	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = ∩ 𝐴 → (Tr 𝑦 ↔ Tr ∩ 𝐴))
68	66, 67	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ∩ 𝐴 → ((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) ↔ (∩ 𝐴 ⊊ 𝑡 ∧ Tr ∩ 𝐴)))
69		eleq1 2900	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ∩ 𝐴 → (𝑦 ∈ 𝑡 ↔ ∩ 𝐴 ∈ 𝑡))
70	68, 69	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ∩ 𝐴 → (((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) ↔ ((∩ 𝐴 ⊊ 𝑡 ∧ Tr ∩ 𝐴) → ∩ 𝐴 ∈ 𝑡)))
71	70	spcgv 3595	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∩ 𝐴 ∈ V → (∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → ((∩ 𝐴 ⊊ 𝑡 ∧ Tr ∩ 𝐴) → ∩ 𝐴 ∈ 𝑡)))
72	41, 71	sylbi 219	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ≠ ∅ → (∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → ((∩ 𝐴 ⊊ 𝑡 ∧ Tr ∩ 𝐴) → ∩ 𝐴 ∈ 𝑡)))
73	72	imp 409	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)) → ((∩ 𝐴 ⊊ 𝑡 ∧ Tr ∩ 𝐴) → ∩ 𝐴 ∈ 𝑡))
74	73	expd 418	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)) → (∩ 𝐴 ⊊ 𝑡 → (Tr ∩ 𝐴 → ∩ 𝐴 ∈ 𝑡)))
75	65, 74	syl5bir 245	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)) → ((∩ 𝐴 ⊆ 𝑡 ∧ ¬ ∩ 𝐴 = 𝑡) → (Tr ∩ 𝐴 → ∩ 𝐴 ∈ 𝑡)))
76	75	exp4b 433	. . . . . . . . . . . . . . . . . 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 483	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (𝑡 ∈ 𝐴 → (∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → (Tr ∩ 𝐴 → (¬ ∩ 𝐴 = 𝑡 → ∩ 𝐴 ∈ 𝑡)))))
81	63, 80	mpdd 43	. . . . . . . . . . . . 13 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (𝑡 ∈ 𝐴 → (Tr ∩ 𝐴 → (¬ ∩ 𝐴 = 𝑡 → ∩ 𝐴 ∈ 𝑡))))
82	81	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (𝑡 ∈ 𝐴 → (Tr ∩ 𝐴 → (¬ ∩ 𝐴 = 𝑡 → ∩ 𝐴 ∈ 𝑡))))
83	56, 82	mpid 44	. . . . . . . . . . 11 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (𝑡 ∈ 𝐴 → (¬ ∩ 𝐴 = 𝑡 → ∩ 𝐴 ∈ 𝑡)))
84	54, 83	syl7bi 257	. . . . . . . . . 10 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (𝑡 ∈ 𝐴 → (¬ 𝑡 = ∩ 𝐴 → ∩ 𝐴 ∈ 𝑡)))
85	84	ralrimiv 3181	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → ∀𝑡 ∈ 𝐴 (¬ 𝑡 = ∩ 𝐴 → ∩ 𝐴 ∈ 𝑡))
86		ralim 3162	. . . . . . . . 9 ⊢ (∀𝑡 ∈ 𝐴 (¬ 𝑡 = ∩ 𝐴 → ∩ 𝐴 ∈ 𝑡) → (∀𝑡 ∈ 𝐴 ¬ 𝑡 = ∩ 𝐴 → ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡))
87	85, 86	syl 17	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (∀𝑡 ∈ 𝐴 ¬ 𝑡 = ∩ 𝐴 → ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡))
88	52, 87	syl5bi 244	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (¬ ∩ 𝐴 ∈ 𝐴 → ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡))
89		elintg 4877	. . . . . . . . 9 ⊢ (∩ 𝐴 ∈ V → (∩ 𝐴 ∈ ∩ 𝐴 ↔ ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡))
90	41, 89	sylbi 219	. . . . . . . 8 ⊢ (𝐴 ≠ ∅ → (∩ 𝐴 ∈ ∩ 𝐴 ↔ ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡))
91	90	ad2antrr 724	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (∩ 𝐴 ∈ ∩ 𝐴 ↔ ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡))
92	88, 91	sylibrd 261	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (¬ ∩ 𝐴 ∈ 𝐴 → ∩ 𝐴 ∈ ∩ 𝐴))
93	48, 92	mt3d 150	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → ∩ 𝐴 ∈ 𝐴)
94	93	ex 415	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) → ∩ 𝐴 ∈ 𝐴))
95	94	ancld 553	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) ∧ ∩ 𝐴 ∈ 𝐴)))
96	40, 95	syl5 34	. 2 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → ((Tr ∩ 𝐴 ∧ ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) ∧ ∩ 𝐴 ∈ 𝐴)))
97	8, 39, 96	mp2and 697	1 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) ∧ ∩ 𝐴 ∈ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1531   = wceq 1533  ∃wex 1776   ∈ wcel 2110   ≠ wne 3016  ∀wral 3138  ∃wrex 3139  Vcvv 3495   ⊆ wss 3936   ⊊ wpss 3937  ∅c0 4291  ∪ cuni 4832  ∩ cint 4869  Tr wtr 5165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pr 5322  ax-un 7455

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-pw 4541  df-sn 4562  df-pr 4564  df-uni 4833  df-int 4870  df-iun 4914  df-iin 4915  df-tr 5166  df-suc 6192

This theorem is referenced by:  dfon2lem9  33031