bnj557

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	bnj557.3	⊢ 𝐷 = ( ω ∖ { ∅ } )
	bnj557.16	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } )
	bnj557.17	⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
	bnj557.18	⊢ ( 𝜎 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) )
	bnj557.19	⊢ ( 𝜂 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
	bnj557.20	⊢ ( 𝜁 ↔ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖 ) )
	bnj557.21	⊢ 𝐵 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
	bnj557.22	⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
	bnj557.23	⊢ 𝐾 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
	bnj557.24	⊢ 𝐿 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
	bnj557.25	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , 𝐶 ⟩ } )
	bnj557.28	⊢ ( 𝜑′ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
	bnj557.29	⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑚 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj557.36	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → 𝐺 Fn 𝑛 )
Assertion	bnj557	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜁 ) → ( 𝐺 ‘ 𝑚 ) = 𝐿 )

Proof

Step	Hyp	Ref	Expression
1		bnj557.3	⊢ 𝐷 = ( ω ∖ { ∅ } )
2		bnj557.16	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } )
3		bnj557.17	⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
4		bnj557.18	⊢ ( 𝜎 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) )
5		bnj557.19	⊢ ( 𝜂 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
6		bnj557.20	⊢ ( 𝜁 ↔ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖 ) )
7		bnj557.21	⊢ 𝐵 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
8		bnj557.22	⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
9		bnj557.23	⊢ 𝐾 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
10		bnj557.24	⊢ 𝐿 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
11		bnj557.25	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , 𝐶 ⟩ } )
12		bnj557.28	⊢ ( 𝜑′ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
13		bnj557.29	⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑚 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
14		bnj557.36	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → 𝐺 Fn 𝑛 )
15		3an4anass	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ 𝜁 ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ) ∧ ( 𝜂 ∧ 𝜁 ) ) )
16	4 5	bnj556	⊢ ( 𝜂 → 𝜎 )
17	16	3anim3i	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) )
18		vex	⊢ 𝑖 ∈ V
19	18	bnj216	⊢ ( 𝑚 = suc 𝑖 → 𝑖 ∈ 𝑚 )
20	6 19	bnj837	⊢ ( 𝜁 → 𝑖 ∈ 𝑚 )
21	17 20	anim12i	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ 𝜁 ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ) )
22	15 21	sylbir	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ) ∧ ( 𝜂 ∧ 𝜁 ) ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ) )
23	5	bnj1254	⊢ ( 𝜂 → 𝑚 = suc 𝑝 )
24	6	simp3bi	⊢ ( 𝜁 → 𝑚 = suc 𝑖 )
25		bnj551	⊢ ( ( 𝑚 = suc 𝑝 ∧ 𝑚 = suc 𝑖 ) → 𝑝 = 𝑖 )
26	23 24 25	syl2an	⊢ ( ( 𝜂 ∧ 𝜁 ) → 𝑝 = 𝑖 )
27	26	adantl	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ) ∧ ( 𝜂 ∧ 𝜁 ) ) → 𝑝 = 𝑖 )
28	22 27	jca	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ) ∧ ( 𝜂 ∧ 𝜁 ) ) → ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ) ∧ 𝑝 = 𝑖 ) )
29		bnj256	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜁 ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ) ∧ ( 𝜂 ∧ 𝜁 ) ) )
30		df-3an	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ∧ 𝑝 = 𝑖 ) ↔ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ) ∧ 𝑝 = 𝑖 ) )
31	28 29 30	3imtr4i	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜁 ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ∧ 𝑝 = 𝑖 ) )
32	12 13 1 2 3 4 8 11 7 9 10 14	bnj553	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ∧ 𝑝 = 𝑖 ) → ( 𝐺 ‘ 𝑚 ) = 𝐿 )
33	31 32	syl	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜁 ) → ( 𝐺 ‘ 𝑚 ) = 𝐿 )

Metamath Proof Explorer

Theorem bnj557

Proof