Theorem bnj1014

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	bnj1014.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
	bnj1014.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj1014.13	⊢ 𝐷 = ( ω ∖ { ∅ } )
	bnj1014.14	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
Assertion	bnj1014	⊢ ( ( 𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔 ) → ( 𝑔 ‘ 𝑗 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		bnj1014.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
2		bnj1014.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3		bnj1014.13	⊢ 𝐷 = ( ω ∖ { ∅ } )
4		bnj1014.14	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
5		nfcv	⊢ Ⅎ 𝑖 𝐷
6	1 2	bnj911	⊢ ( ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) → ∀ 𝑖 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
7	6	nf5i	⊢ Ⅎ 𝑖 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 )
8	5 7	nfrexw	⊢ Ⅎ 𝑖 ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 )
9	8	nfab	⊢ Ⅎ 𝑖 { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
10	4 9	nfcxfr	⊢ Ⅎ 𝑖 𝐵
11	10	nfcri	⊢ Ⅎ 𝑖 𝑔 ∈ 𝐵
12		nfv	⊢ Ⅎ 𝑖 𝑗 ∈ dom 𝑔
13	11 12	nfan	⊢ Ⅎ 𝑖 ( 𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔 )
14		nfv	⊢ Ⅎ 𝑖 ( 𝑔 ‘ 𝑗 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 )
15	13 14	nfim	⊢ Ⅎ 𝑖 ( ( 𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔 ) → ( 𝑔 ‘ 𝑗 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
16	15	nf5ri	⊢ ( ( ( 𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔 ) → ( 𝑔 ‘ 𝑗 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → ∀ 𝑖 ( ( 𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔 ) → ( 𝑔 ‘ 𝑗 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
17		eleq1w	⊢ ( 𝑗 = 𝑖 → ( 𝑗 ∈ dom 𝑔 ↔ 𝑖 ∈ dom 𝑔 ) )
18	17	anbi2d	⊢ ( 𝑗 = 𝑖 → ( ( 𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔 ) ↔ ( 𝑔 ∈ 𝐵 ∧ 𝑖 ∈ dom 𝑔 ) ) )
19		fveq2	⊢ ( 𝑗 = 𝑖 → ( 𝑔 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑖 ) )
20	19	sseq1d	⊢ ( 𝑗 = 𝑖 → ( ( 𝑔 ‘ 𝑗 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ↔ ( 𝑔 ‘ 𝑖 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
21	18 20	imbi12d	⊢ ( 𝑗 = 𝑖 → ( ( ( 𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔 ) → ( 𝑔 ‘ 𝑗 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ↔ ( ( 𝑔 ∈ 𝐵 ∧ 𝑖 ∈ dom 𝑔 ) → ( 𝑔 ‘ 𝑖 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) )
22	21	equcoms	⊢ ( 𝑖 = 𝑗 → ( ( ( 𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔 ) → ( 𝑔 ‘ 𝑗 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ↔ ( ( 𝑔 ∈ 𝐵 ∧ 𝑖 ∈ dom 𝑔 ) → ( 𝑔 ‘ 𝑖 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) )
23	4	bnj1317	⊢ ( 𝑔 ∈ 𝐵 → ∀ 𝑓 𝑔 ∈ 𝐵 )
24	23	nf5i	⊢ Ⅎ 𝑓 𝑔 ∈ 𝐵
25		nfv	⊢ Ⅎ 𝑓 𝑖 ∈ dom 𝑔
26	24 25	nfan	⊢ Ⅎ 𝑓 ( 𝑔 ∈ 𝐵 ∧ 𝑖 ∈ dom 𝑔 )
27		nfv	⊢ Ⅎ 𝑓 ( 𝑔 ‘ 𝑖 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 )
28	26 27	nfim	⊢ Ⅎ 𝑓 ( ( 𝑔 ∈ 𝐵 ∧ 𝑖 ∈ dom 𝑔 ) → ( 𝑔 ‘ 𝑖 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
29		eleq1w	⊢ ( 𝑓 = 𝑔 → ( 𝑓 ∈ 𝐵 ↔ 𝑔 ∈ 𝐵 ) )
30		dmeq	⊢ ( 𝑓 = 𝑔 → dom 𝑓 = dom 𝑔 )
31	30	eleq2d	⊢ ( 𝑓 = 𝑔 → ( 𝑖 ∈ dom 𝑓 ↔ 𝑖 ∈ dom 𝑔 ) )
32	29 31	anbi12d	⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 ∈ 𝐵 ∧ 𝑖 ∈ dom 𝑓 ) ↔ ( 𝑔 ∈ 𝐵 ∧ 𝑖 ∈ dom 𝑔 ) ) )
33		fveq1	⊢ ( 𝑓 = 𝑔 → ( 𝑓 ‘ 𝑖 ) = ( 𝑔 ‘ 𝑖 ) )
34	33	sseq1d	⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 ‘ 𝑖 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ↔ ( 𝑔 ‘ 𝑖 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
35	32 34	imbi12d	⊢ ( 𝑓 = 𝑔 → ( ( ( 𝑓 ∈ 𝐵 ∧ 𝑖 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑖 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ↔ ( ( 𝑔 ∈ 𝐵 ∧ 𝑖 ∈ dom 𝑔 ) → ( 𝑔 ‘ 𝑖 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) )
36		ssiun2	⊢ ( 𝑖 ∈ dom 𝑓 → ( 𝑓 ‘ 𝑖 ) ⊆ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) )
37		ssiun2	⊢ ( 𝑓 ∈ 𝐵 → ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ⊆ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) )
38	1 2 3 4	bnj882	⊢ trCl ( 𝑋 , 𝐴 , 𝑅 ) = ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 )
39	37 38	sseqtrrdi	⊢ ( 𝑓 ∈ 𝐵 → ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
40	36 39	sylan9ssr	⊢ ( ( 𝑓 ∈ 𝐵 ∧ 𝑖 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑖 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
41	28 35 40	chvarfv	⊢ ( ( 𝑔 ∈ 𝐵 ∧ 𝑖 ∈ dom 𝑔 ) → ( 𝑔 ‘ 𝑖 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
42	22 41	speivw	⊢ ∃ 𝑖 ( ( 𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔 ) → ( 𝑔 ‘ 𝑗 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
43	16 42	bnj1131	⊢ ( ( 𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔 ) → ( 𝑔 ‘ 𝑗 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )