bnj229

Description: Technical lemma for bnj517 . 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
	Hypothesis	bnj229.1	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	Assertion	bnj229	⊢ ( ( 𝑛 ∈ 𝑁 ∧ ( suc 𝑚 = 𝑛 ∧ 𝑚 ∈ ω ∧ 𝜓 ) ) → ( 𝐹 ‘ 𝑛 ) ⊆ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		bnj229.1	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
2		bnj213	⊢ pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐴
3	2	bnj226	⊢ ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐴
4	1	bnj222	⊢ ( 𝜓 ↔ ∀ 𝑚 ∈ ω ( suc 𝑚 ∈ 𝑁 → ( 𝐹 ‘ suc 𝑚 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
5	4	bnj228	⊢ ( ( 𝑚 ∈ ω ∧ 𝜓 ) → ( suc 𝑚 ∈ 𝑁 → ( 𝐹 ‘ suc 𝑚 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
6	5	adantl	⊢ ( ( suc 𝑚 = 𝑛 ∧ ( 𝑚 ∈ ω ∧ 𝜓 ) ) → ( suc 𝑚 ∈ 𝑁 → ( 𝐹 ‘ suc 𝑚 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
7		eleq1	⊢ ( suc 𝑚 = 𝑛 → ( suc 𝑚 ∈ 𝑁 ↔ 𝑛 ∈ 𝑁 ) )
8		fveqeq2	⊢ ( suc 𝑚 = 𝑛 → ( ( 𝐹 ‘ suc 𝑚 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝐹 ‘ 𝑛 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
9	7 8	imbi12d	⊢ ( suc 𝑚 = 𝑛 → ( ( suc 𝑚 ∈ 𝑁 → ( 𝐹 ‘ suc 𝑚 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( 𝑛 ∈ 𝑁 → ( 𝐹 ‘ 𝑛 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
10	9	adantr	⊢ ( ( suc 𝑚 = 𝑛 ∧ ( 𝑚 ∈ ω ∧ 𝜓 ) ) → ( ( suc 𝑚 ∈ 𝑁 → ( 𝐹 ‘ suc 𝑚 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( 𝑛 ∈ 𝑁 → ( 𝐹 ‘ 𝑛 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
11	6 10	mpbid	⊢ ( ( suc 𝑚 = 𝑛 ∧ ( 𝑚 ∈ ω ∧ 𝜓 ) ) → ( 𝑛 ∈ 𝑁 → ( 𝐹 ‘ 𝑛 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
12	11	3impb	⊢ ( ( suc 𝑚 = 𝑛 ∧ 𝑚 ∈ ω ∧ 𝜓 ) → ( 𝑛 ∈ 𝑁 → ( 𝐹 ‘ 𝑛 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
13	12	impcom	⊢ ( ( 𝑛 ∈ 𝑁 ∧ ( suc 𝑚 = 𝑛 ∧ 𝑚 ∈ ω ∧ 𝜓 ) ) → ( 𝐹 ‘ 𝑛 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
14	3 13	bnj1262	⊢ ( ( 𝑛 ∈ 𝑁 ∧ ( suc 𝑚 = 𝑛 ∧ 𝑚 ∈ ω ∧ 𝜓 ) ) → ( 𝐹 ‘ 𝑛 ) ⊆ 𝐴 )

Metamath Proof Explorer

Theorem bnj229

Proof