Metamath Proof Explorer

Theorem bnj1015

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1015.1 ⊢ φ ↔ f ⁡ ∅ = pred X A R
bnj1015.2 ⊢ ψ ↔ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
bnj1015.13 ⊢ D = ω ∖ ∅
bnj1015.14 ⊢ B = f | ∃ n ∈ D f Fn n ∧ φ ∧ ψ
bnj1015.15 ⊢ G ∈ V
bnj1015.16 ⊢ J ∈ V
Assertion bnj1015 ⊢ G ∈ B ∧ J ∈ dom ⁡ G → G ⁡ J ⊆ trCl X A R

Proof

Step Hyp Ref Expression
1 bnj1015.1 ⊢ φ ↔ f ⁡ ∅ = pred X A R
2 bnj1015.2 ⊢ ψ ↔ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
3 bnj1015.13 ⊢ D = ω ∖ ∅
4 bnj1015.14 ⊢ B = f | ∃ n ∈ D f Fn n ∧ φ ∧ ψ
5 bnj1015.15 ⊢ G ∈ V
6 bnj1015.16 ⊢ J ∈ V
7 6 elexi ⊢ J ∈ V
8 eleq1 ⊢ j = J → j ∈ dom ⁡ G ↔ J ∈ dom ⁡ G
9 8 anbi2d ⊢ j = J → G ∈ B ∧ j ∈ dom ⁡ G ↔ G ∈ B ∧ J ∈ dom ⁡ G
10 fveq2 ⊢ j = J → G ⁡ j = G ⁡ J
11 10 sseq1d ⊢ j = J → G ⁡ j ⊆ trCl X A R ↔ G ⁡ J ⊆ trCl X A R
12 9 11 imbi12d ⊢ j = J → G ∈ B ∧ j ∈ dom ⁡ G → G ⁡ j ⊆ trCl X A R ↔ G ∈ B ∧ J ∈ dom ⁡ G → G ⁡ J ⊆ trCl X A R
13 5 elexi ⊢ G ∈ V
14 eleq1 ⊢ g = G → g ∈ B ↔ G ∈ B
15 dmeq ⊢ g = G → dom ⁡ g = dom ⁡ G
16 15 eleq2d ⊢ g = G → j ∈ dom ⁡ g ↔ j ∈ dom ⁡ G
17 14 16 anbi12d ⊢ g = G → g ∈ B ∧ j ∈ dom ⁡ g ↔ G ∈ B ∧ j ∈ dom ⁡ G
18 fveq1 ⊢ g = G → g ⁡ j = G ⁡ j
19 18 sseq1d ⊢ g = G → g ⁡ j ⊆ trCl X A R ↔ G ⁡ j ⊆ trCl X A R
20 17 19 imbi12d ⊢ g = G → g ∈ B ∧ j ∈ dom ⁡ g → g ⁡ j ⊆ trCl X A R ↔ G ∈ B ∧ j ∈ dom ⁡ G → G ⁡ j ⊆ trCl X A R
21 1 2 3 4 bnj1014 ⊢ g ∈ B ∧ j ∈ dom ⁡ g → g ⁡ j ⊆ trCl X A R
22 13 20 21 vtocl ⊢ G ∈ B ∧ j ∈ dom ⁡ G → G ⁡ j ⊆ trCl X A R
23 7 12 22 vtocl ⊢ G ∈ B ∧ J ∈ dom ⁡ G → G ⁡ J ⊆ trCl X A R