Theorem dfon2lem8 35751

Description: Lemma for dfon2 35753. 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 3448	. . . . . . 7 ⊢ 𝑥 ∈ V
2		dfon2lem3 35746	. . . . . . 7 ⊢ (𝑥 ∈ V → (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (Tr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧)))
3	1, 2	ax-mp 5	. . . . . 6 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (Tr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧))
4	3	simpld 494	. . . . 5 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → Tr 𝑥)
5	4	ralimi 3066	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑥 ∈ 𝐴 Tr 𝑥)
6		trint 5227	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∩ 𝐴)
7	5, 6	syl 17	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → Tr ∩ 𝐴)
8	7	adantl 481	. 2 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → Tr ∩ 𝐴)
9	1	dfon2lem7 35750	. . . . . . 7 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
10	9	alrimiv 1927	. . . . . 6 ⊢ (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
11	10	ralimi 3066	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑥 ∈ 𝐴 ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
12		df-ral 3045	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
13		19.21v 1939	. . . . . . . 8 ⊢ (∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) ↔ (𝑥 ∈ 𝐴 → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
14	13	albii 1819	. . . . . . 7 ⊢ (∀𝑥∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
15	12, 14	bitr4i 278	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑥∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
16		impexp 450	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ (𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
17	16	2albii 1820	. . . . . . 7 ⊢ (∀𝑥∀𝑤((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑥∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))))
18		eluni2 4871	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ∪ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥)
19	18	biimpi 216	. . . . . . . . . 10 ⊢ (𝑤 ∈ ∪ 𝐴 → ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥)
20	19	imim1i 63	. . . . . . . . 9 ⊢ ((∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → (𝑤 ∈ ∪ 𝐴 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
21	20	alimi 1811	. . . . . . . 8 ⊢ (∀𝑤(∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → ∀𝑤(𝑤 ∈ ∪ 𝐴 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
22		alcom 2160	. . . . . . . . 9 ⊢ (∀𝑥∀𝑤((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑤∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
23		19.23v 1942	. . . . . . . . . . 11 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
24		df-rex 3054	. . . . . . . . . . . 12 ⊢ (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥))
25	24	imbi1i 349	. . . . . . . . . . 11 ⊢ ((∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
26	23, 25	bitr4i 278	. . . . . . . . . 10 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
27	26	albii 1819	. . . . . . . . 9 ⊢ (∀𝑤∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
28	22, 27	bitri 275	. . . . . . . 8 ⊢ (∀𝑥∀𝑤((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))
29		df-ral 3045	. . . . . . . 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 4930	. . . . 5 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴)
36		ssralv 4012	. . . . 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 35749	. . 3 ⊢ ((Tr ∩ 𝐴 ∧ ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴))
41		intex 5294	. . . . . . . . . . 11 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)
42		dfon2lem3 35746	. . . . . . . . . . 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 35668	. . . . . . . 8 ⊢ (∀𝑡 ∈ ∩ 𝐴 ¬ 𝑡 ∈ 𝑡 → ¬ ∩ 𝐴 ∈ ∩ 𝐴)
47	45, 46	syl 17	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → ¬ ∩ 𝐴 ∈ ∩ 𝐴)
48	47	adantlr 715	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → ¬ ∩ 𝐴 ∈ ∩ 𝐴)
49		risset 3210	. . . . . . . . . 10 ⊢ (∩ 𝐴 ∈ 𝐴 ↔ ∃𝑡 ∈ 𝐴 𝑡 = ∩ 𝐴)
50	49	notbii 320	. . . . . . . . 9 ⊢ (¬ ∩ 𝐴 ∈ 𝐴 ↔ ¬ ∃𝑡 ∈ 𝐴 𝑡 = ∩ 𝐴)
51		ralnex 3055	. . . . . . . . 9 ⊢ (∀𝑡 ∈ 𝐴 ¬ 𝑡 = ∩ 𝐴 ↔ ¬ ∃𝑡 ∈ 𝐴 𝑡 = ∩ 𝐴)
52	50, 51	bitr4i 278	. . . . . . . 8 ⊢ (¬ ∩ 𝐴 ∈ 𝐴 ↔ ∀𝑡 ∈ 𝐴 ¬ 𝑡 = ∩ 𝐴)
53		eqcom 2736	. . . . . . . . . . . 12 ⊢ (𝑡 = ∩ 𝐴 ↔ ∩ 𝐴 = 𝑡)
54	53	notbii 320	. . . . . . . . . . 11 ⊢ (¬ 𝑡 = ∩ 𝐴 ↔ ¬ ∩ 𝐴 = 𝑡)
55	44	simpld 494	. . . . . . . . . . . . 13 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → Tr ∩ 𝐴)
56	55	adantlr 715	. . . . . . . . . . . 12 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → Tr ∩ 𝐴)
57		psseq2 4050	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑡 → (𝑦 ⊊ 𝑥 ↔ 𝑦 ⊊ 𝑡))
58	57	anbi1d 631	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑡 → ((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) ↔ (𝑦 ⊊ 𝑡 ∧ Tr 𝑦)))
59		elequ2 2124	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑡 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑡))
60	58, 59	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑡 → (((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) ↔ ((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)))
61	60	albidv 1920	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑡 → (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) ↔ ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)))
62	61	rspccv 3582	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (𝑡 ∈ 𝐴 → ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)))
63	62	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (𝑡 ∈ 𝐴 → ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)))
64		intss1 4923	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑡)
65		dfpss2 4047	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∩ 𝐴 ⊊ 𝑡 ↔ (∩ 𝐴 ⊆ 𝑡 ∧ ¬ ∩ 𝐴 = 𝑡))
66		psseq1 4049	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = ∩ 𝐴 → (𝑦 ⊊ 𝑡 ↔ ∩ 𝐴 ⊊ 𝑡))
67		treq 5217	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = ∩ 𝐴 → (Tr 𝑦 ↔ Tr ∩ 𝐴))
68	66, 67	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ∩ 𝐴 → ((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) ↔ (∩ 𝐴 ⊊ 𝑡 ∧ Tr ∩ 𝐴)))
69		eleq1 2816	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ∩ 𝐴 → (𝑦 ∈ 𝑡 ↔ ∩ 𝐴 ∈ 𝑡))
70	68, 69	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ∩ 𝐴 → (((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) ↔ ((∩ 𝐴 ⊊ 𝑡 ∧ Tr ∩ 𝐴) → ∩ 𝐴 ∈ 𝑡)))
71	70	spcgv 3559	. . . . . . . . . . . . . . . . . . . . . . 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 3124	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → ∀𝑡 ∈ 𝐴 (¬ 𝑡 = ∩ 𝐴 → ∩ 𝐴 ∈ 𝑡))
86		ralim 3069	. . . . . . . . 9 ⊢ (∀𝑡 ∈ 𝐴 (¬ 𝑡 = ∩ 𝐴 → ∩ 𝐴 ∈ 𝑡) → (∀𝑡 ∈ 𝐴 ¬ 𝑡 = ∩ 𝐴 → ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡))
87	85, 86	syl 17	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (∀𝑡 ∈ 𝐴 ¬ 𝑡 = ∩ 𝐴 → ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡))
88	52, 87	biimtrid 242	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (¬ ∩ 𝐴 ∈ 𝐴 → ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡))
89		elintg 4914	. . . . . . . . 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 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  Vcvv 3444   ⊆ wss 3911   ⊊ wpss 3912  ∅c0 4292  ∪ cuni 4867  ∩ cint 4906  Tr wtr 5209

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 5246  ax-nul 5256  ax-pr 5382  ax-un 7691

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 3403  df-v 3446  df-sbc 3751  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-pw 4561  df-sn 4586  df-pr 4588  df-uni 4868  df-int 4907  df-iun 4953  df-iin 4954  df-tr 5210  df-suc 6326

This theorem is referenced by:  dfon2lem9  35752