bnj1133

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	bnj1133.3	⊢ 𝐷 = ( ω ∖ { ∅ } )
	bnj1133.5	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
	bnj1133.7	⊢ ( 𝜏 ↔ ∀ 𝑗 ∈ 𝑛 ( 𝑗 E 𝑖 → [ 𝑗 / 𝑖 ] 𝜃 ) )
	bnj1133.8	⊢ ( ( 𝑖 ∈ 𝑛 ∧ 𝜏 ) → 𝜃 )
Assertion	bnj1133	⊢ ( 𝜒 → ∀ 𝑖 ∈ 𝑛 𝜃 )

Proof

Step	Hyp	Ref	Expression
1		bnj1133.3	⊢ 𝐷 = ( ω ∖ { ∅ } )
2		bnj1133.5	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
3		bnj1133.7	⊢ ( 𝜏 ↔ ∀ 𝑗 ∈ 𝑛 ( 𝑗 E 𝑖 → [ 𝑗 / 𝑖 ] 𝜃 ) )
4		bnj1133.8	⊢ ( ( 𝑖 ∈ 𝑛 ∧ 𝜏 ) → 𝜃 )
5	1	bnj1071	⊢ ( 𝑛 ∈ 𝐷 → E Fr 𝑛 )
6	2 5	bnj769	⊢ ( 𝜒 → E Fr 𝑛 )
7		impexp	⊢ ( ( ( 𝑖 ∈ 𝑛 ∧ 𝜏 ) → 𝜃 ) ↔ ( 𝑖 ∈ 𝑛 → ( 𝜏 → 𝜃 ) ) )
8	7	bicomi	⊢ ( ( 𝑖 ∈ 𝑛 → ( 𝜏 → 𝜃 ) ) ↔ ( ( 𝑖 ∈ 𝑛 ∧ 𝜏 ) → 𝜃 ) )
9	8	albii	⊢ ( ∀ 𝑖 ( 𝑖 ∈ 𝑛 → ( 𝜏 → 𝜃 ) ) ↔ ∀ 𝑖 ( ( 𝑖 ∈ 𝑛 ∧ 𝜏 ) → 𝜃 ) )
10	9 4	mpgbir	⊢ ∀ 𝑖 ( 𝑖 ∈ 𝑛 → ( 𝜏 → 𝜃 ) )
11		df-ral	⊢ ( ∀ 𝑖 ∈ 𝑛 ( 𝜏 → 𝜃 ) ↔ ∀ 𝑖 ( 𝑖 ∈ 𝑛 → ( 𝜏 → 𝜃 ) ) )
12	10 11	mpbir	⊢ ∀ 𝑖 ∈ 𝑛 ( 𝜏 → 𝜃 )
13		vex	⊢ 𝑛 ∈ V
14	13 3	bnj110	⊢ ( ( E Fr 𝑛 ∧ ∀ 𝑖 ∈ 𝑛 ( 𝜏 → 𝜃 ) ) → ∀ 𝑖 ∈ 𝑛 𝜃 )
15	6 12 14	sylancl	⊢ ( 𝜒 → ∀ 𝑖 ∈ 𝑛 𝜃 )

Metamath Proof Explorer

Theorem bnj1133

Proof