Theorem bnj543

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	bnj543.1	⊢ ( 𝜑′ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
	bnj543.2	⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑚 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj543.3	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } )
	bnj543.4	⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
	bnj543.5	⊢ ( 𝜎 ↔ ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) )
Assertion	bnj543	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → 𝐺 Fn 𝑛 )

Proof

Step	Hyp	Ref	Expression
1		bnj543.1	⊢ ( 𝜑′ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
2		bnj543.2	⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑚 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3		bnj543.3	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } )
4		bnj543.4	⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
5		bnj543.5	⊢ ( 𝜎 ↔ ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) )
6		bnj257	⊢ ( ( ( 𝜑′ ∧ 𝜓′ ) ∧ ( 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = suc 𝑚 ∧ 𝑓 Fn 𝑚 ) ↔ ( ( 𝜑′ ∧ 𝜓′ ) ∧ ( 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑓 Fn 𝑚 ∧ 𝑛 = suc 𝑚 ) )
7		bnj268	⊢ ( ( ( 𝜑′ ∧ 𝜓′ ) ∧ ( 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑓 Fn 𝑚 ∧ 𝑛 = suc 𝑚 ) ↔ ( ( 𝜑′ ∧ 𝜓′ ) ∧ 𝑓 Fn 𝑚 ∧ ( 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = suc 𝑚 ) )
8	6 7	bitri	⊢ ( ( ( 𝜑′ ∧ 𝜓′ ) ∧ ( 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = suc 𝑚 ∧ 𝑓 Fn 𝑚 ) ↔ ( ( 𝜑′ ∧ 𝜓′ ) ∧ 𝑓 Fn 𝑚 ∧ ( 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = suc 𝑚 ) )
9		bnj253	⊢ ( ( ( 𝜑′ ∧ 𝜓′ ) ∧ ( 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = suc 𝑚 ∧ 𝑓 Fn 𝑚 ) ↔ ( ( ( 𝜑′ ∧ 𝜓′ ) ∧ ( 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ) ∧ 𝑛 = suc 𝑚 ∧ 𝑓 Fn 𝑚 ) )
10		bnj256	⊢ ( ( ( 𝜑′ ∧ 𝜓′ ) ∧ 𝑓 Fn 𝑚 ∧ ( 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = suc 𝑚 ) ↔ ( ( ( 𝜑′ ∧ 𝜓′ ) ∧ 𝑓 Fn 𝑚 ) ∧ ( ( 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = suc 𝑚 ) ) )
11	8 9 10	3bitr3i	⊢ ( ( ( ( 𝜑′ ∧ 𝜓′ ) ∧ ( 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ) ∧ 𝑛 = suc 𝑚 ∧ 𝑓 Fn 𝑚 ) ↔ ( ( ( 𝜑′ ∧ 𝜓′ ) ∧ 𝑓 Fn 𝑚 ) ∧ ( ( 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = suc 𝑚 ) ) )
12		bnj256	⊢ ( ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ↔ ( ( 𝜑′ ∧ 𝜓′ ) ∧ ( 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ) )
13	12	3anbi1i	⊢ ( ( ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = suc 𝑚 ∧ 𝑓 Fn 𝑚 ) ↔ ( ( ( 𝜑′ ∧ 𝜓′ ) ∧ ( 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ) ∧ 𝑛 = suc 𝑚 ∧ 𝑓 Fn 𝑚 ) )
14		bnj170	⊢ ( ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) ↔ ( ( 𝜑′ ∧ 𝜓′ ) ∧ 𝑓 Fn 𝑚 ) )
15	4 14	bitri	⊢ ( 𝜏 ↔ ( ( 𝜑′ ∧ 𝜓′ ) ∧ 𝑓 Fn 𝑚 ) )
16		3anan32	⊢ ( ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) ↔ ( ( 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = suc 𝑚 ) )
17	5 16	bitri	⊢ ( 𝜎 ↔ ( ( 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = suc 𝑚 ) )
18	15 17	anbi12i	⊢ ( ( 𝜏 ∧ 𝜎 ) ↔ ( ( ( 𝜑′ ∧ 𝜓′ ) ∧ 𝑓 Fn 𝑚 ) ∧ ( ( 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = suc 𝑚 ) ) )
19	11 13 18	3bitr4ri	⊢ ( ( 𝜏 ∧ 𝜎 ) ↔ ( ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = suc 𝑚 ∧ 𝑓 Fn 𝑚 ) )
20	19	anbi2i	⊢ ( ( 𝑅 FrSe 𝐴 ∧ ( 𝜏 ∧ 𝜎 ) ) ↔ ( 𝑅 FrSe 𝐴 ∧ ( ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = suc 𝑚 ∧ 𝑓 Fn 𝑚 ) ) )
21		3anass	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ↔ ( 𝑅 FrSe 𝐴 ∧ ( 𝜏 ∧ 𝜎 ) ) )
22		bnj252	⊢ ( ( 𝑅 FrSe 𝐴 ∧ ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = suc 𝑚 ∧ 𝑓 Fn 𝑚 ) ↔ ( 𝑅 FrSe 𝐴 ∧ ( ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = suc 𝑚 ∧ 𝑓 Fn 𝑚 ) ) )
23	20 21 22	3bitr4i	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ↔ ( 𝑅 FrSe 𝐴 ∧ ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = suc 𝑚 ∧ 𝑓 Fn 𝑚 ) )
24		df-suc	⊢ suc 𝑚 = ( 𝑚 ∪ { 𝑚 } )
25	24	eqeq2i	⊢ ( 𝑛 = suc 𝑚 ↔ 𝑛 = ( 𝑚 ∪ { 𝑚 } ) )
26	25	3anbi2i	⊢ ( ( ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = suc 𝑚 ∧ 𝑓 Fn 𝑚 ) ↔ ( ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = ( 𝑚 ∪ { 𝑚 } ) ∧ 𝑓 Fn 𝑚 ) )
27	26	anbi2i	⊢ ( ( 𝑅 FrSe 𝐴 ∧ ( ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = suc 𝑚 ∧ 𝑓 Fn 𝑚 ) ) ↔ ( 𝑅 FrSe 𝐴 ∧ ( ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = ( 𝑚 ∪ { 𝑚 } ) ∧ 𝑓 Fn 𝑚 ) ) )
28		bnj252	⊢ ( ( 𝑅 FrSe 𝐴 ∧ ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = ( 𝑚 ∪ { 𝑚 } ) ∧ 𝑓 Fn 𝑚 ) ↔ ( 𝑅 FrSe 𝐴 ∧ ( ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = ( 𝑚 ∪ { 𝑚 } ) ∧ 𝑓 Fn 𝑚 ) ) )
29	27 22 28	3bitr4i	⊢ ( ( 𝑅 FrSe 𝐴 ∧ ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = suc 𝑚 ∧ 𝑓 Fn 𝑚 ) ↔ ( 𝑅 FrSe 𝐴 ∧ ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = ( 𝑚 ∪ { 𝑚 } ) ∧ 𝑓 Fn 𝑚 ) )
30		biid	⊢ ( ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ↔ ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) )
31	1 2 3 30	bnj535	⊢ ( ( 𝑅 FrSe 𝐴 ∧ ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = ( 𝑚 ∪ { 𝑚 } ) ∧ 𝑓 Fn 𝑚 ) → 𝐺 Fn 𝑛 )
32	29 31	sylbi	⊢ ( ( 𝑅 FrSe 𝐴 ∧ ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ∧ 𝑛 = suc 𝑚 ∧ 𝑓 Fn 𝑚 ) → 𝐺 Fn 𝑛 )
33	23 32	sylbi	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → 𝐺 Fn 𝑛 )