This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lbsextlem3

Description: Lemma for lbsext . A chain in S has an upper bound in S . (Contributed by Mario Carneiro, 25-Jun-2014)

Ref Expression
Hypotheses lbsext.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lbsext.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
lbsext.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lbsext.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lbsext.c ⊢ ( 𝜑 → 𝐶 ⊆ 𝑉 )
lbsext.x ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) )
lbsext.s ⊢ 𝑆 = { 𝑧 ∈ 𝒫 𝑉 ∣ ( 𝐶 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ) }
lbsext.p ⊢ 𝑃 = ( LSubSp ‘ 𝑊 )
lbsext.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
lbsext.z ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
lbsext.r ⊢ ( 𝜑 → [⊊] Or 𝐴 )
lbsext.t ⊢ 𝑇 = ∪ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) )
Assertion lbsextlem3 ( 𝜑 → ∪ 𝐴 ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 lbsext.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lbsext.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
3 lbsext.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 lbsext.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
5 lbsext.c ⊢ ( 𝜑 → 𝐶 ⊆ 𝑉 )
6 lbsext.x ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) )
7 lbsext.s ⊢ 𝑆 = { 𝑧 ∈ 𝒫 𝑉 ∣ ( 𝐶 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ) }
8 lbsext.p ⊢ 𝑃 = ( LSubSp ‘ 𝑊 )
9 lbsext.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
10 lbsext.z ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
11 lbsext.r ⊢ ( 𝜑 → [⊊] Or 𝐴 )
12 lbsext.t ⊢ 𝑇 = ∪ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) )
13 7 ssrab3 ⊢ 𝑆 ⊆ 𝒫 𝑉
14 9 13 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ 𝒫 𝑉 )
15 sspwuni ⊢ ( 𝐴 ⊆ 𝒫 𝑉 ↔ ∪ 𝐴 ⊆ 𝑉 )
16 14 15 sylib ⊢ ( 𝜑 → ∪ 𝐴 ⊆ 𝑉 )
17 1 fvexi ⊢ 𝑉 ∈ V
18 17 elpw2 ⊢ ( ∪ 𝐴 ∈ 𝒫 𝑉 ↔ ∪ 𝐴 ⊆ 𝑉 )
19 16 18 sylibr ⊢ ( 𝜑 → ∪ 𝐴 ∈ 𝒫 𝑉 )
20 ssintub ⊢ 𝐶 ⊆ ∩ { 𝑧 ∈ 𝒫 𝑉 ∣ 𝐶 ⊆ 𝑧 }
21 simpl ⊢ ( ( 𝐶 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ) → 𝐶 ⊆ 𝑧 )
22 21 a1i ⊢ ( 𝑧 ∈ 𝒫 𝑉 → ( ( 𝐶 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ) → 𝐶 ⊆ 𝑧 ) )
23 22 ss2rabi ⊢ { 𝑧 ∈ 𝒫 𝑉 ∣ ( 𝐶 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ) } ⊆ { 𝑧 ∈ 𝒫 𝑉 ∣ 𝐶 ⊆ 𝑧 }
24 7 23 eqsstri ⊢ 𝑆 ⊆ { 𝑧 ∈ 𝒫 𝑉 ∣ 𝐶 ⊆ 𝑧 }
25 9 24 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ { 𝑧 ∈ 𝒫 𝑉 ∣ 𝐶 ⊆ 𝑧 } )
26 intss ⊢ ( 𝐴 ⊆ { 𝑧 ∈ 𝒫 𝑉 ∣ 𝐶 ⊆ 𝑧 } → ∩ { 𝑧 ∈ 𝒫 𝑉 ∣ 𝐶 ⊆ 𝑧 } ⊆ ∩ 𝐴 )
27 25 26 syl ⊢ ( 𝜑 → ∩ { 𝑧 ∈ 𝒫 𝑉 ∣ 𝐶 ⊆ 𝑧 } ⊆ ∩ 𝐴 )
28 20 27 sstrid ⊢ ( 𝜑 → 𝐶 ⊆ ∩ 𝐴 )
29 intssuni ⊢ ( 𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴 )
30 10 29 syl ⊢ ( 𝜑 → ∩ 𝐴 ⊆ ∪ 𝐴 )
31 28 30 sstrd ⊢ ( 𝜑 → 𝐶 ⊆ ∪ 𝐴 )
32 eluni2 ⊢ ( 𝑥 ∈ ∪ 𝐴 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 )
33 simpll1 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) → 𝜑 )
34 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
35 4 34 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
36 33 35 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) → 𝑊 ∈ LMod )
37 33 9 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) → 𝐴 ⊆ 𝑆 )
38 33 11 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) → [⊊] Or 𝐴 )
39 simpll2 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) → 𝑦 ∈ 𝐴 )
40 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) → 𝑢 ∈ 𝐴 )
41 sorpssun ⊢ ( ( [⊊] Or 𝐴 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ) ) → ( 𝑦 ∪ 𝑢 ) ∈ 𝐴 )
42 38 39 40 41 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) → ( 𝑦 ∪ 𝑢 ) ∈ 𝐴 )
43 37 42 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) → ( 𝑦 ∪ 𝑢 ) ∈ 𝑆 )
44 13 43 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) → ( 𝑦 ∪ 𝑢 ) ∈ 𝒫 𝑉 )
45 44 elpwid ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) → ( 𝑦 ∪ 𝑢 ) ⊆ 𝑉 )
46 45 ssdifssd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) → ( ( 𝑦 ∪ 𝑢 ) ∖ { 𝑥 } ) ⊆ 𝑉 )
47 ssun2 ⊢ 𝑢 ⊆ ( 𝑦 ∪ 𝑢 )
48 ssdif ⊢ ( 𝑢 ⊆ ( 𝑦 ∪ 𝑢 ) → ( 𝑢 ∖ { 𝑥 } ) ⊆ ( ( 𝑦 ∪ 𝑢 ) ∖ { 𝑥 } ) )
49 47 48 mp1i ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) → ( 𝑢 ∖ { 𝑥 } ) ⊆ ( ( 𝑦 ∪ 𝑢 ) ∖ { 𝑥 } ) )
50 1 3 lspss ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑦 ∪ 𝑢 ) ∖ { 𝑥 } ) ⊆ 𝑉 ∧ ( 𝑢 ∖ { 𝑥 } ) ⊆ ( ( 𝑦 ∪ 𝑢 ) ∖ { 𝑥 } ) ) → ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ⊆ ( 𝑁 ‘ ( ( 𝑦 ∪ 𝑢 ) ∖ { 𝑥 } ) ) )
51 36 46 49 50 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) → ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ⊆ ( 𝑁 ‘ ( ( 𝑦 ∪ 𝑢 ) ∖ { 𝑥 } ) ) )
52 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) → 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) )
53 51 52 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) → 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑦 ∪ 𝑢 ) ∖ { 𝑥 } ) ) )
54 sseq2 ⊢ ( 𝑧 = ( 𝑦 ∪ 𝑢 ) → ( 𝐶 ⊆ 𝑧 ↔ 𝐶 ⊆ ( 𝑦 ∪ 𝑢 ) ) )
55 difeq1 ⊢ ( 𝑧 = ( 𝑦 ∪ 𝑢 ) → ( 𝑧 ∖ { 𝑥 } ) = ( ( 𝑦 ∪ 𝑢 ) ∖ { 𝑥 } ) )
56 55 fveq2d ⊢ ( 𝑧 = ( 𝑦 ∪ 𝑢 ) → ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) = ( 𝑁 ‘ ( ( 𝑦 ∪ 𝑢 ) ∖ { 𝑥 } ) ) )
57 56 eleq2d ⊢ ( 𝑧 = ( 𝑦 ∪ 𝑢 ) → ( 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ↔ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑦 ∪ 𝑢 ) ∖ { 𝑥 } ) ) ) )
58 57 notbid ⊢ ( 𝑧 = ( 𝑦 ∪ 𝑢 ) → ( ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ↔ ¬ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑦 ∪ 𝑢 ) ∖ { 𝑥 } ) ) ) )
59 58 raleqbi1dv ⊢ ( 𝑧 = ( 𝑦 ∪ 𝑢 ) → ( ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ↔ ∀ 𝑥 ∈ ( 𝑦 ∪ 𝑢 ) ¬ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑦 ∪ 𝑢 ) ∖ { 𝑥 } ) ) ) )
60 54 59 anbi12d ⊢ ( 𝑧 = ( 𝑦 ∪ 𝑢 ) → ( ( 𝐶 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ) ↔ ( 𝐶 ⊆ ( 𝑦 ∪ 𝑢 ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ 𝑢 ) ¬ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑦 ∪ 𝑢 ) ∖ { 𝑥 } ) ) ) ) )
61 60 7 elrab2 ⊢ ( ( 𝑦 ∪ 𝑢 ) ∈ 𝑆 ↔ ( ( 𝑦 ∪ 𝑢 ) ∈ 𝒫 𝑉 ∧ ( 𝐶 ⊆ ( 𝑦 ∪ 𝑢 ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ 𝑢 ) ¬ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑦 ∪ 𝑢 ) ∖ { 𝑥 } ) ) ) ) )
62 61 simprbi ⊢ ( ( 𝑦 ∪ 𝑢 ) ∈ 𝑆 → ( 𝐶 ⊆ ( 𝑦 ∪ 𝑢 ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ 𝑢 ) ¬ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑦 ∪ 𝑢 ) ∖ { 𝑥 } ) ) ) )
63 62 simprd ⊢ ( ( 𝑦 ∪ 𝑢 ) ∈ 𝑆 → ∀ 𝑥 ∈ ( 𝑦 ∪ 𝑢 ) ¬ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑦 ∪ 𝑢 ) ∖ { 𝑥 } ) ) )
64 43 63 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) → ∀ 𝑥 ∈ ( 𝑦 ∪ 𝑢 ) ¬ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑦 ∪ 𝑢 ) ∖ { 𝑥 } ) ) )
65 simpll3 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) → 𝑥 ∈ 𝑦 )
66 elun1 ⊢ ( 𝑥 ∈ 𝑦 → 𝑥 ∈ ( 𝑦 ∪ 𝑢 ) )
67 65 66 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) → 𝑥 ∈ ( 𝑦 ∪ 𝑢 ) )
68 rsp ⊢ ( ∀ 𝑥 ∈ ( 𝑦 ∪ 𝑢 ) ¬ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑦 ∪ 𝑢 ) ∖ { 𝑥 } ) ) → ( 𝑥 ∈ ( 𝑦 ∪ 𝑢 ) → ¬ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑦 ∪ 𝑢 ) ∖ { 𝑥 } ) ) ) )
69 64 67 68 sylc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) → ¬ 𝑥 ∈ ( 𝑁 ‘ ( ( 𝑦 ∪ 𝑢 ) ∖ { 𝑥 } ) ) )
70 53 69 pm2.65da ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑢 ∈ 𝐴 ) → ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) )
71 70 nrexdv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) → ¬ ∃ 𝑢 ∈ 𝐴 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) )
72 1 2 3 4 5 6 7 8 9 10 11 12 lbsextlem2 ⊢ ( 𝜑 → ( 𝑇 ∈ 𝑃 ∧ ( ∪ 𝐴 ∖ { 𝑥 } ) ⊆ 𝑇 ) )
73 72 simpld ⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
74 1 8 lssss ⊢ ( 𝑇 ∈ 𝑃 → 𝑇 ⊆ 𝑉 )
75 73 74 syl ⊢ ( 𝜑 → 𝑇 ⊆ 𝑉 )
76 72 simprd ⊢ ( 𝜑 → ( ∪ 𝐴 ∖ { 𝑥 } ) ⊆ 𝑇 )
77 1 3 lspss ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ ( ∪ 𝐴 ∖ { 𝑥 } ) ⊆ 𝑇 ) → ( 𝑁 ‘ ( ∪ 𝐴 ∖ { 𝑥 } ) ) ⊆ ( 𝑁 ‘ 𝑇 ) )
78 35 75 76 77 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ ( ∪ 𝐴 ∖ { 𝑥 } ) ) ⊆ ( 𝑁 ‘ 𝑇 ) )
79 8 3 lspid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑃 ) → ( 𝑁 ‘ 𝑇 ) = 𝑇 )
80 35 73 79 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑇 ) = 𝑇 )
81 78 80 sseqtrd ⊢ ( 𝜑 → ( 𝑁 ‘ ( ∪ 𝐴 ∖ { 𝑥 } ) ) ⊆ 𝑇 )
82 81 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) → ( 𝑁 ‘ ( ∪ 𝐴 ∖ { 𝑥 } ) ) ⊆ 𝑇 )
83 82 12 sseqtrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) → ( 𝑁 ‘ ( ∪ 𝐴 ∖ { 𝑥 } ) ) ⊆ ∪ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) )
84 83 sseld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) → ( 𝑥 ∈ ( 𝑁 ‘ ( ∪ 𝐴 ∖ { 𝑥 } ) ) → 𝑥 ∈ ∪ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) )
85 eliun ⊢ ( 𝑥 ∈ ∪ 𝑢 ∈ 𝐴 ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ↔ ∃ 𝑢 ∈ 𝐴 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) )
86 84 85 imbitrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) → ( 𝑥 ∈ ( 𝑁 ‘ ( ∪ 𝐴 ∖ { 𝑥 } ) ) → ∃ 𝑢 ∈ 𝐴 𝑥 ∈ ( 𝑁 ‘ ( 𝑢 ∖ { 𝑥 } ) ) ) )
87 71 86 mtod ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) → ¬ 𝑥 ∈ ( 𝑁 ‘ ( ∪ 𝐴 ∖ { 𝑥 } ) ) )
88 87 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ ( 𝑁 ‘ ( ∪ 𝐴 ∖ { 𝑥 } ) ) ) )
89 32 88 biimtrid ⊢ ( 𝜑 → ( 𝑥 ∈ ∪ 𝐴 → ¬ 𝑥 ∈ ( 𝑁 ‘ ( ∪ 𝐴 ∖ { 𝑥 } ) ) ) )
90 89 ralrimiv ⊢ ( 𝜑 → ∀ 𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ ( 𝑁 ‘ ( ∪ 𝐴 ∖ { 𝑥 } ) ) )
91 31 90 jca ⊢ ( 𝜑 → ( 𝐶 ⊆ ∪ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ ( 𝑁 ‘ ( ∪ 𝐴 ∖ { 𝑥 } ) ) ) )
92 sseq2 ⊢ ( 𝑧 = ∪ 𝐴 → ( 𝐶 ⊆ 𝑧 ↔ 𝐶 ⊆ ∪ 𝐴 ) )
93 difeq1 ⊢ ( 𝑧 = ∪ 𝐴 → ( 𝑧 ∖ { 𝑥 } ) = ( ∪ 𝐴 ∖ { 𝑥 } ) )
94 93 fveq2d ⊢ ( 𝑧 = ∪ 𝐴 → ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) = ( 𝑁 ‘ ( ∪ 𝐴 ∖ { 𝑥 } ) ) )
95 94 eleq2d ⊢ ( 𝑧 = ∪ 𝐴 → ( 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ↔ 𝑥 ∈ ( 𝑁 ‘ ( ∪ 𝐴 ∖ { 𝑥 } ) ) ) )
96 95 notbid ⊢ ( 𝑧 = ∪ 𝐴 → ( ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ↔ ¬ 𝑥 ∈ ( 𝑁 ‘ ( ∪ 𝐴 ∖ { 𝑥 } ) ) ) )
97 96 raleqbi1dv ⊢ ( 𝑧 = ∪ 𝐴 → ( ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ↔ ∀ 𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ ( 𝑁 ‘ ( ∪ 𝐴 ∖ { 𝑥 } ) ) ) )
98 92 97 anbi12d ⊢ ( 𝑧 = ∪ 𝐴 → ( ( 𝐶 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ) ↔ ( 𝐶 ⊆ ∪ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ ( 𝑁 ‘ ( ∪ 𝐴 ∖ { 𝑥 } ) ) ) ) )
99 98 7 elrab2 ⊢ ( ∪ 𝐴 ∈ 𝑆 ↔ ( ∪ 𝐴 ∈ 𝒫 𝑉 ∧ ( 𝐶 ⊆ ∪ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ ( 𝑁 ‘ ( ∪ 𝐴 ∖ { 𝑥 } ) ) ) ) )
100 19 91 99 sylanbrc ⊢ ( 𝜑 → ∪ 𝐴 ∈ 𝑆 )