Theorem bnj553

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	bnj553.1	⊢ ( 𝜑′ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
	bnj553.2	⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑚 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj553.3	⊢ 𝐷 = ( ω ∖ { ∅ } )
	bnj553.4	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } )
	bnj553.5	⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
	bnj553.6	⊢ ( 𝜎 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) )
	bnj553.7	⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
	bnj553.8	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , 𝐶 ⟩ } )
	bnj553.9	⊢ 𝐵 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
	bnj553.10	⊢ 𝐾 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
	bnj553.11	⊢ 𝐿 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
	bnj553.12	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → 𝐺 Fn 𝑛 )
Assertion	bnj553	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ∧ 𝑝 = 𝑖 ) → ( 𝐺 ‘ 𝑚 ) = 𝐿 )

Proof

Step	Hyp	Ref	Expression
1		bnj553.1	⊢ ( 𝜑′ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
2		bnj553.2	⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑚 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3		bnj553.3	⊢ 𝐷 = ( ω ∖ { ∅ } )
4		bnj553.4	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } )
5		bnj553.5	⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
6		bnj553.6	⊢ ( 𝜎 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) )
7		bnj553.7	⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
8		bnj553.8	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , 𝐶 ⟩ } )
9		bnj553.9	⊢ 𝐵 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
10		bnj553.10	⊢ 𝐾 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
11		bnj553.11	⊢ 𝐿 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
12		bnj553.12	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → 𝐺 Fn 𝑛 )
13	12	fnfund	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → Fun 𝐺 )
14		opex	⊢ ⟨ 𝑚 , 𝐶 ⟩ ∈ V
15	14	snid	⊢ ⟨ 𝑚 , 𝐶 ⟩ ∈ { ⟨ 𝑚 , 𝐶 ⟩ }
16		elun2	⊢ ( ⟨ 𝑚 , 𝐶 ⟩ ∈ { ⟨ 𝑚 , 𝐶 ⟩ } → ⟨ 𝑚 , 𝐶 ⟩ ∈ ( 𝑓 ∪ { ⟨ 𝑚 , 𝐶 ⟩ } ) )
17	15 16	ax-mp	⊢ ⟨ 𝑚 , 𝐶 ⟩ ∈ ( 𝑓 ∪ { ⟨ 𝑚 , 𝐶 ⟩ } )
18	17 8	eleqtrri	⊢ ⟨ 𝑚 , 𝐶 ⟩ ∈ 𝐺
19		funopfv	⊢ ( Fun 𝐺 → ( ⟨ 𝑚 , 𝐶 ⟩ ∈ 𝐺 → ( 𝐺 ‘ 𝑚 ) = 𝐶 ) )
20	13 18 19	mpisyl	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → ( 𝐺 ‘ 𝑚 ) = 𝐶 )
21	20	3ad2ant1	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ∧ 𝑝 = 𝑖 ) → ( 𝐺 ‘ 𝑚 ) = 𝐶 )
22		fveq2	⊢ ( 𝑝 = 𝑖 → ( 𝐺 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑖 ) )
23	22	bnj1113	⊢ ( 𝑝 = 𝑖 → ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
24	23 11 10	3eqtr4g	⊢ ( 𝑝 = 𝑖 → 𝐿 = 𝐾 )
25	24	3ad2ant3	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ∧ 𝑝 = 𝑖 ) → 𝐿 = 𝐾 )
26	5 9 10 4 12	bnj548	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ) → 𝐵 = 𝐾 )
27	26	3adant3	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ∧ 𝑝 = 𝑖 ) → 𝐵 = 𝐾 )
28		fveq2	⊢ ( 𝑝 = 𝑖 → ( 𝑓 ‘ 𝑝 ) = ( 𝑓 ‘ 𝑖 ) )
29	28	bnj1113	⊢ ( 𝑝 = 𝑖 → ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
30	9 7	eqeq12i	⊢ ( 𝐵 = 𝐶 ↔ ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
31		eqcom	⊢ ( ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
32	30 31	bitri	⊢ ( 𝐵 = 𝐶 ↔ ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
33	29 32	sylibr	⊢ ( 𝑝 = 𝑖 → 𝐵 = 𝐶 )
34	33	3ad2ant3	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ∧ 𝑝 = 𝑖 ) → 𝐵 = 𝐶 )
35	25 27 34	3eqtr2rd	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ∧ 𝑝 = 𝑖 ) → 𝐶 = 𝐿 )
36	21 35	eqtrd	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ∧ 𝑝 = 𝑖 ) → ( 𝐺 ‘ 𝑚 ) = 𝐿 )