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 ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
bnj1015.2 ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
bnj1015.13 𝐷 = ( ω ∖ { ∅ } )
bnj1015.14 𝐵 = { 𝑓 ∣ ∃ 𝑛𝐷 ( 𝑓 Fn 𝑛𝜑𝜓 ) }
bnj1015.15 𝐺𝑉
bnj1015.16 𝐽𝑉
Assertion bnj1015 ( ( 𝐺𝐵𝐽 ∈ dom 𝐺 ) → ( 𝐺𝐽 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )

Proof

Step Hyp Ref Expression
1 bnj1015.1 ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
2 bnj1015.2 ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3 bnj1015.13 𝐷 = ( ω ∖ { ∅ } )
4 bnj1015.14 𝐵 = { 𝑓 ∣ ∃ 𝑛𝐷 ( 𝑓 Fn 𝑛𝜑𝜓 ) }
5 bnj1015.15 𝐺𝑉
6 bnj1015.16 𝐽𝑉
7 6 elexi 𝐽 ∈ V
8 eleq1 ( 𝑗 = 𝐽 → ( 𝑗 ∈ dom 𝐺𝐽 ∈ dom 𝐺 ) )
9 8 anbi2d ( 𝑗 = 𝐽 → ( ( 𝐺𝐵𝑗 ∈ dom 𝐺 ) ↔ ( 𝐺𝐵𝐽 ∈ dom 𝐺 ) ) )
10 fveq2 ( 𝑗 = 𝐽 → ( 𝐺𝑗 ) = ( 𝐺𝐽 ) )
11 10 sseq1d ( 𝑗 = 𝐽 → ( ( 𝐺𝑗 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ↔ ( 𝐺𝐽 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
12 9 11 imbi12d ( 𝑗 = 𝐽 → ( ( ( 𝐺𝐵𝑗 ∈ dom 𝐺 ) → ( 𝐺𝑗 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ↔ ( ( 𝐺𝐵𝐽 ∈ dom 𝐺 ) → ( 𝐺𝐽 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) )
13 5 elexi 𝐺 ∈ V
14 eleq1 ( 𝑔 = 𝐺 → ( 𝑔𝐵𝐺𝐵 ) )
15 dmeq ( 𝑔 = 𝐺 → dom 𝑔 = dom 𝐺 )
16 15 eleq2d ( 𝑔 = 𝐺 → ( 𝑗 ∈ dom 𝑔𝑗 ∈ dom 𝐺 ) )
17 14 16 anbi12d ( 𝑔 = 𝐺 → ( ( 𝑔𝐵𝑗 ∈ dom 𝑔 ) ↔ ( 𝐺𝐵𝑗 ∈ dom 𝐺 ) ) )
18 fveq1 ( 𝑔 = 𝐺 → ( 𝑔𝑗 ) = ( 𝐺𝑗 ) )
19 18 sseq1d ( 𝑔 = 𝐺 → ( ( 𝑔𝑗 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ↔ ( 𝐺𝑗 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
20 17 19 imbi12d ( 𝑔 = 𝐺 → ( ( ( 𝑔𝐵𝑗 ∈ dom 𝑔 ) → ( 𝑔𝑗 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ↔ ( ( 𝐺𝐵𝑗 ∈ dom 𝐺 ) → ( 𝐺𝑗 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) )
21 1 2 3 4 bnj1014 ( ( 𝑔𝐵𝑗 ∈ dom 𝑔 ) → ( 𝑔𝑗 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
22 13 20 21 vtocl ( ( 𝐺𝐵𝑗 ∈ dom 𝐺 ) → ( 𝐺𝑗 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
23 7 12 22 vtocl ( ( 𝐺𝐵𝐽 ∈ dom 𝐺 ) → ( 𝐺𝐽 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )