Theorem 1stcrest

Description: A subspace of a first-countable space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Assertion	1stcrest	⊢ ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ 1stω )

Proof

Step	Hyp	Ref	Expression
1		1stctop	⊢ ( 𝐽 ∈ 1stω → 𝐽 ∈ Top )
2		resttop	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ Top )
3	1 2	sylan	⊢ ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ Top )
4		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
5	4	restuni2	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∩ ∪ 𝐽 ) = ∪ ( 𝐽 ↾t 𝐴 ) )
6	1 5	sylan	⊢ ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∩ ∪ 𝐽 ) = ∪ ( 𝐽 ↾t 𝐴 ) )
7	6	eleq2d	⊢ ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ↔ 𝑥 ∈ ∪ ( 𝐽 ↾t 𝐴 ) ) )
8	7	biimpar	⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ∪ ( 𝐽 ↾t 𝐴 ) ) → 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) )
9		simpl	⊢ ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) → 𝐽 ∈ 1stω )
10		elinel2	⊢ ( 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) → 𝑥 ∈ ∪ 𝐽 )
11	4	1stcclb	⊢ ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ∪ 𝐽 ) → ∃ 𝑡 ∈ 𝒫 𝐽 ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) )
12	9 10 11	syl2an	⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) → ∃ 𝑡 ∈ 𝒫 𝐽 ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) )
13		simplll	⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → 𝐽 ∈ 1stω )
14		elpwi	⊢ ( 𝑡 ∈ 𝒫 𝐽 → 𝑡 ⊆ 𝐽 )
15	14	ad2antrl	⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → 𝑡 ⊆ 𝐽 )
16		ssrest	⊢ ( ( 𝐽 ∈ 1stω ∧ 𝑡 ⊆ 𝐽 ) → ( 𝑡 ↾t 𝐴 ) ⊆ ( 𝐽 ↾t 𝐴 ) )
17	13 15 16	syl2anc	⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → ( 𝑡 ↾t 𝐴 ) ⊆ ( 𝐽 ↾t 𝐴 ) )
18		ovex	⊢ ( 𝐽 ↾t 𝐴 ) ∈ V
19	18	elpw2	⊢ ( ( 𝑡 ↾t 𝐴 ) ∈ 𝒫 ( 𝐽 ↾t 𝐴 ) ↔ ( 𝑡 ↾t 𝐴 ) ⊆ ( 𝐽 ↾t 𝐴 ) )
20	17 19	sylibr	⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → ( 𝑡 ↾t 𝐴 ) ∈ 𝒫 ( 𝐽 ↾t 𝐴 ) )
21		vex	⊢ 𝑡 ∈ V
22		simpllr	⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → 𝐴 ∈ 𝑉 )
23		restval	⊢ ( ( 𝑡 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝑡 ↾t 𝐴 ) = ran ( 𝑣 ∈ 𝑡 ↦ ( 𝑣 ∩ 𝐴 ) ) )
24	21 22 23	sylancr	⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → ( 𝑡 ↾t 𝐴 ) = ran ( 𝑣 ∈ 𝑡 ↦ ( 𝑣 ∩ 𝐴 ) ) )
25		simprrl	⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → 𝑡 ≼ ω )
26		1stcrestlem	⊢ ( 𝑡 ≼ ω → ran ( 𝑣 ∈ 𝑡 ↦ ( 𝑣 ∩ 𝐴 ) ) ≼ ω )
27	25 26	syl	⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → ran ( 𝑣 ∈ 𝑡 ↦ ( 𝑣 ∩ 𝐴 ) ) ≼ ω )
28	24 27	eqbrtrd	⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → ( 𝑡 ↾t 𝐴 ) ≼ ω )
29	1	ad3antrrr	⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → 𝐽 ∈ Top )
30		elrest	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ∃ 𝑎 ∈ 𝐽 𝑧 = ( 𝑎 ∩ 𝐴 ) ) )
31	29 22 30	syl2anc	⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → ( 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ∃ 𝑎 ∈ 𝐽 𝑧 = ( 𝑎 ∩ 𝐴 ) ) )
32		r19.29	⊢ ( ( ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ∧ ∃ 𝑎 ∈ 𝐽 𝑧 = ( 𝑎 ∩ 𝐴 ) ) → ∃ 𝑎 ∈ 𝐽 ( ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ∧ 𝑧 = ( 𝑎 ∩ 𝐴 ) ) )
33		simprr	⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) → 𝑥 ∈ 𝐴 )
34	33	a1d	⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝑥 ∈ 𝑦 → 𝑥 ∈ 𝐴 ) )
35	34	ancld	⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝑥 ∈ 𝑦 → ( 𝑥 ∈ 𝑦 ∧ 𝑥 ∈ 𝐴 ) ) )
36		elin	⊢ ( 𝑥 ∈ ( 𝑦 ∩ 𝐴 ) ↔ ( 𝑥 ∈ 𝑦 ∧ 𝑥 ∈ 𝐴 ) )
37	35 36	syl6ibr	⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝑥 ∈ 𝑦 → 𝑥 ∈ ( 𝑦 ∩ 𝐴 ) ) )
38		ssrin	⊢ ( 𝑦 ⊆ 𝑎 → ( 𝑦 ∩ 𝐴 ) ⊆ ( 𝑎 ∩ 𝐴 ) )
39	37 38	anim12d1	⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) → ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) → ( 𝑥 ∈ ( 𝑦 ∩ 𝐴 ) ∧ ( 𝑦 ∩ 𝐴 ) ⊆ ( 𝑎 ∩ 𝐴 ) ) ) )
40	39	reximdv	⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) → ( ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ ( 𝑦 ∩ 𝐴 ) ∧ ( 𝑦 ∩ 𝐴 ) ⊆ ( 𝑎 ∩ 𝐴 ) ) ) )
41		vex	⊢ 𝑦 ∈ V
42	41	inex1	⊢ ( 𝑦 ∩ 𝐴 ) ∈ V
43	42	a1i	⊢ ( ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) ∧ 𝑦 ∈ 𝑡 ) → ( 𝑦 ∩ 𝐴 ) ∈ V )
44		simp-4r	⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) → 𝐴 ∈ 𝑉 )
45		elrest	⊢ ( ( 𝑡 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ 𝑡 𝑤 = ( 𝑦 ∩ 𝐴 ) ) )
46	21 44 45	sylancr	⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ 𝑡 𝑤 = ( 𝑦 ∩ 𝐴 ) ) )
47		eleq2	⊢ ( 𝑤 = ( 𝑦 ∩ 𝐴 ) → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ ( 𝑦 ∩ 𝐴 ) ) )
48		sseq1	⊢ ( 𝑤 = ( 𝑦 ∩ 𝐴 ) → ( 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ↔ ( 𝑦 ∩ 𝐴 ) ⊆ ( 𝑎 ∩ 𝐴 ) ) )
49	47 48	anbi12d	⊢ ( 𝑤 = ( 𝑦 ∩ 𝐴 ) → ( ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) ↔ ( 𝑥 ∈ ( 𝑦 ∩ 𝐴 ) ∧ ( 𝑦 ∩ 𝐴 ) ⊆ ( 𝑎 ∩ 𝐴 ) ) ) )
50	49	adantl	⊢ ( ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) ∧ 𝑤 = ( 𝑦 ∩ 𝐴 ) ) → ( ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) ↔ ( 𝑥 ∈ ( 𝑦 ∩ 𝐴 ) ∧ ( 𝑦 ∩ 𝐴 ) ⊆ ( 𝑎 ∩ 𝐴 ) ) ) )
51	43 46 50	rexxfr2d	⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) → ( ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) ↔ ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ ( 𝑦 ∩ 𝐴 ) ∧ ( 𝑦 ∩ 𝐴 ) ⊆ ( 𝑎 ∩ 𝐴 ) ) ) )
52	40 51	sylibrd	⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) → ( ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) ) )
53	52	expr	⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ 𝑎 ∈ 𝐽 ) → ( 𝑥 ∈ 𝐴 → ( ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) ) ) )
54	53	com23	⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ 𝑎 ∈ 𝐽 ) → ( ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) → ( 𝑥 ∈ 𝐴 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) ) ) )
55	54	imim2d	⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ 𝑎 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) → ( 𝑥 ∈ 𝑎 → ( 𝑥 ∈ 𝐴 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) ) ) ) )
56	55	imp4b	⊢ ( ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ 𝑎 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) → ( ( 𝑥 ∈ 𝑎 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) ) )
57		eleq2	⊢ ( 𝑧 = ( 𝑎 ∩ 𝐴 ) → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ( 𝑎 ∩ 𝐴 ) ) )
58		elin	⊢ ( 𝑥 ∈ ( 𝑎 ∩ 𝐴 ) ↔ ( 𝑥 ∈ 𝑎 ∧ 𝑥 ∈ 𝐴 ) )
59	57 58	bitrdi	⊢ ( 𝑧 = ( 𝑎 ∩ 𝐴 ) → ( 𝑥 ∈ 𝑧 ↔ ( 𝑥 ∈ 𝑎 ∧ 𝑥 ∈ 𝐴 ) ) )
60		sseq2	⊢ ( 𝑧 = ( 𝑎 ∩ 𝐴 ) → ( 𝑤 ⊆ 𝑧 ↔ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) )
61	60	anbi2d	⊢ ( 𝑧 = ( 𝑎 ∩ 𝐴 ) → ( ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ↔ ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) ) )
62	61	rexbidv	⊢ ( 𝑧 = ( 𝑎 ∩ 𝐴 ) → ( ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ↔ ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) ) )
63	59 62	imbi12d	⊢ ( 𝑧 = ( 𝑎 ∩ 𝐴 ) → ( ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ↔ ( ( 𝑥 ∈ 𝑎 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) ) ) )
64	56 63	syl5ibrcom	⊢ ( ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ 𝑎 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) → ( 𝑧 = ( 𝑎 ∩ 𝐴 ) → ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
65	64	expimpd	⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ 𝑎 ∈ 𝐽 ) → ( ( ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ∧ 𝑧 = ( 𝑎 ∩ 𝐴 ) ) → ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
66	65	rexlimdva	⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) → ( ∃ 𝑎 ∈ 𝐽 ( ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ∧ 𝑧 = ( 𝑎 ∩ 𝐴 ) ) → ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
67	32 66	syl5	⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) → ( ( ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ∧ ∃ 𝑎 ∈ 𝐽 𝑧 = ( 𝑎 ∩ 𝐴 ) ) → ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
68	67	expd	⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) → ( ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) → ( ∃ 𝑎 ∈ 𝐽 𝑧 = ( 𝑎 ∩ 𝐴 ) → ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) )
69	68	impr	⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) → ( ∃ 𝑎 ∈ 𝐽 𝑧 = ( 𝑎 ∩ 𝐴 ) → ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
70	69	adantrrl	⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → ( ∃ 𝑎 ∈ 𝐽 𝑧 = ( 𝑎 ∩ 𝐴 ) → ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
71	31 70	sylbid	⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → ( 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) → ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
72	71	ralrimiv	⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
73		breq1	⊢ ( 𝑦 = ( 𝑡 ↾t 𝐴 ) → ( 𝑦 ≼ ω ↔ ( 𝑡 ↾t 𝐴 ) ≼ ω ) )
74		rexeq	⊢ ( 𝑦 = ( 𝑡 ↾t 𝐴 ) → ( ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ↔ ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
75	74	imbi2d	⊢ ( 𝑦 = ( 𝑡 ↾t 𝐴 ) → ( ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ↔ ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
76	75	ralbidv	⊢ ( 𝑦 = ( 𝑡 ↾t 𝐴 ) → ( ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ↔ ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
77	73 76	anbi12d	⊢ ( 𝑦 = ( 𝑡 ↾t 𝐴 ) → ( ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ↔ ( ( 𝑡 ↾t 𝐴 ) ≼ ω ∧ ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) )
78	77	rspcev	⊢ ( ( ( 𝑡 ↾t 𝐴 ) ∈ 𝒫 ( 𝐽 ↾t 𝐴 ) ∧ ( ( 𝑡 ↾t 𝐴 ) ≼ ω ∧ ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) → ∃ 𝑦 ∈ 𝒫 ( 𝐽 ↾t 𝐴 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
79	20 28 72 78	syl12anc	⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → ∃ 𝑦 ∈ 𝒫 ( 𝐽 ↾t 𝐴 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
80	12 79	rexlimddv	⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) → ∃ 𝑦 ∈ 𝒫 ( 𝐽 ↾t 𝐴 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
81	8 80	syldan	⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ∪ ( 𝐽 ↾t 𝐴 ) ) → ∃ 𝑦 ∈ 𝒫 ( 𝐽 ↾t 𝐴 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
82	81	ralrimiva	⊢ ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) → ∀ 𝑥 ∈ ∪ ( 𝐽 ↾t 𝐴 ) ∃ 𝑦 ∈ 𝒫 ( 𝐽 ↾t 𝐴 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
83		eqid	⊢ ∪ ( 𝐽 ↾t 𝐴 ) = ∪ ( 𝐽 ↾t 𝐴 )
84	83	is1stc2	⊢ ( ( 𝐽 ↾t 𝐴 ) ∈ 1stω ↔ ( ( 𝐽 ↾t 𝐴 ) ∈ Top ∧ ∀ 𝑥 ∈ ∪ ( 𝐽 ↾t 𝐴 ) ∃ 𝑦 ∈ 𝒫 ( 𝐽 ↾t 𝐴 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) )
85	3 82 84	sylanbrc	⊢ ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ 1stω )