bnj554

Description: Technical lemma for bnj852 . 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	bnj554.19	⊢ ( 𝜂 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
	bnj554.20	⊢ ( 𝜁 ↔ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖 ) )
	bnj554.21	⊢ 𝐾 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
	bnj554.22	⊢ 𝐿 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
	bnj554.23	⊢ 𝐾 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
	bnj554.24	⊢ 𝐿 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
Assertion	bnj554	⊢ ( ( 𝜂 ∧ 𝜁 ) → ( ( 𝐺 ‘ 𝑚 ) = 𝐿 ↔ ( 𝐺 ‘ suc 𝑖 ) = 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		bnj554.19	⊢ ( 𝜂 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
2		bnj554.20	⊢ ( 𝜁 ↔ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖 ) )
3		bnj554.21	⊢ 𝐾 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
4		bnj554.22	⊢ 𝐿 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
5		bnj554.23	⊢ 𝐾 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
6		bnj554.24	⊢ 𝐿 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
7	1	bnj1254	⊢ ( 𝜂 → 𝑚 = suc 𝑝 )
8	2	simp3bi	⊢ ( 𝜁 → 𝑚 = suc 𝑖 )
9		simpr	⊢ ( ( 𝑚 = suc 𝑝 ∧ 𝑚 = suc 𝑖 ) → 𝑚 = suc 𝑖 )
10		bnj551	⊢ ( ( 𝑚 = suc 𝑝 ∧ 𝑚 = suc 𝑖 ) → 𝑝 = 𝑖 )
11		fveq2	⊢ ( 𝑚 = suc 𝑖 → ( 𝐺 ‘ 𝑚 ) = ( 𝐺 ‘ suc 𝑖 ) )
12		fveq2	⊢ ( 𝑝 = 𝑖 → ( 𝐺 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑖 ) )
13		iuneq1	⊢ ( ( 𝐺 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑖 ) → ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
14	13 6 5	3eqtr4g	⊢ ( ( 𝐺 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑖 ) → 𝐿 = 𝐾 )
15	12 14	syl	⊢ ( 𝑝 = 𝑖 → 𝐿 = 𝐾 )
16	11 15	eqeqan12d	⊢ ( ( 𝑚 = suc 𝑖 ∧ 𝑝 = 𝑖 ) → ( ( 𝐺 ‘ 𝑚 ) = 𝐿 ↔ ( 𝐺 ‘ suc 𝑖 ) = 𝐾 ) )
17	9 10 16	syl2anc	⊢ ( ( 𝑚 = suc 𝑝 ∧ 𝑚 = suc 𝑖 ) → ( ( 𝐺 ‘ 𝑚 ) = 𝐿 ↔ ( 𝐺 ‘ suc 𝑖 ) = 𝐾 ) )
18	7 8 17	syl2an	⊢ ( ( 𝜂 ∧ 𝜁 ) → ( ( 𝐺 ‘ 𝑚 ) = 𝐿 ↔ ( 𝐺 ‘ suc 𝑖 ) = 𝐾 ) )

Metamath Proof Explorer

Theorem bnj554

Proof