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 ( 𝑋 , 𝐴 , 𝑅 ) )