bnj1123

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	bnj1123.4	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj1123.3	⊢ 𝐾 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
	bnj1123.1	⊢ ( 𝜂 ↔ ( ( 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) )
	bnj1123.2	⊢ ( 𝜂′ ↔ [ 𝑗 / 𝑖 ] 𝜂 )
Assertion	bnj1123	⊢ ( 𝜂′ ↔ ( ( 𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		bnj1123.4	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
2		bnj1123.3	⊢ 𝐾 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
3		bnj1123.1	⊢ ( 𝜂 ↔ ( ( 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) )
4		bnj1123.2	⊢ ( 𝜂′ ↔ [ 𝑗 / 𝑖 ] 𝜂 )
5	3	sbcbii	⊢ ( [ 𝑗 / 𝑖 ] 𝜂 ↔ [ 𝑗 / 𝑖 ] ( ( 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) )
6		nfcv	⊢ Ⅎ 𝑖 𝐷
7		nfv	⊢ Ⅎ 𝑖 𝑓 Fn 𝑛
8		nfv	⊢ Ⅎ 𝑖 𝜑
9	1	bnj1095	⊢ ( 𝜓 → ∀ 𝑖 𝜓 )
10	9	nf5i	⊢ Ⅎ 𝑖 𝜓
11	7 8 10	nf3an	⊢ Ⅎ 𝑖 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 )
12	6 11	nfrexw	⊢ Ⅎ 𝑖 ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 )
13	12	nfab	⊢ Ⅎ 𝑖 { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
14	2 13	nfcxfr	⊢ Ⅎ 𝑖 𝐾
15	14	nfcri	⊢ Ⅎ 𝑖 𝑓 ∈ 𝐾
16		nfv	⊢ Ⅎ 𝑖 𝑗 ∈ dom 𝑓
17	15 16	nfan	⊢ Ⅎ 𝑖 ( 𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓 )
18		nfv	⊢ Ⅎ 𝑖 ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵
19	17 18	nfim	⊢ Ⅎ 𝑖 ( ( 𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 )
20		eleq1w	⊢ ( 𝑖 = 𝑗 → ( 𝑖 ∈ dom 𝑓 ↔ 𝑗 ∈ dom 𝑓 ) )
21	20	anbi2d	⊢ ( 𝑖 = 𝑗 → ( ( 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) ↔ ( 𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓 ) ) )
22		fveq2	⊢ ( 𝑖 = 𝑗 → ( 𝑓 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑗 ) )
23	22	sseq1d	⊢ ( 𝑖 = 𝑗 → ( ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ↔ ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) )
24	21 23	imbi12d	⊢ ( 𝑖 = 𝑗 → ( ( ( 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) ↔ ( ( 𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) ) )
25	19 24	sbciegf	⊢ ( 𝑗 ∈ V → ( [ 𝑗 / 𝑖 ] ( ( 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) ↔ ( ( 𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) ) )
26	25	elv	⊢ ( [ 𝑗 / 𝑖 ] ( ( 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) ↔ ( ( 𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) )
27	4 5 26	3bitri	⊢ ( 𝜂′ ↔ ( ( 𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) )

Metamath Proof Explorer

Theorem bnj1123

Proof