bnj1006

Description: Technical lemma for bnj69 . 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	bnj1006.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
	bnj1006.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj1006.3	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
	bnj1006.4	⊢ ( 𝜃 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj1006.5	⊢ ( 𝜏 ↔ ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) )
	bnj1006.6	⊢ ( 𝜂 ↔ ( 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
	bnj1006.7	⊢ ( 𝜑′ ↔ [ 𝑝 / 𝑛 ] 𝜑 )
	bnj1006.8	⊢ ( 𝜓′ ↔ [ 𝑝 / 𝑛 ] 𝜓 )
	bnj1006.9	⊢ ( 𝜒′ ↔ [ 𝑝 / 𝑛 ] 𝜒 )
	bnj1006.10	⊢ ( 𝜑″ ↔ [ 𝐺 / 𝑓 ] 𝜑′ )
	bnj1006.11	⊢ ( 𝜓″ ↔ [ 𝐺 / 𝑓 ] 𝜓′ )
	bnj1006.12	⊢ ( 𝜒″ ↔ [ 𝐺 / 𝑓 ] 𝜒′ )
	bnj1006.13	⊢ 𝐷 = ( ω ∖ { ∅ } )
	bnj1006.15	⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 )
	bnj1006.16	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
	bnj1006.28	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → ( 𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) )
Assertion	bnj1006	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ ( 𝐺 ‘ suc 𝑖 ) )

Proof

Step	Hyp	Ref	Expression
1		bnj1006.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
2		bnj1006.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3		bnj1006.3	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
4		bnj1006.4	⊢ ( 𝜃 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
5		bnj1006.5	⊢ ( 𝜏 ↔ ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) )
6		bnj1006.6	⊢ ( 𝜂 ↔ ( 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
7		bnj1006.7	⊢ ( 𝜑′ ↔ [ 𝑝 / 𝑛 ] 𝜑 )
8		bnj1006.8	⊢ ( 𝜓′ ↔ [ 𝑝 / 𝑛 ] 𝜓 )
9		bnj1006.9	⊢ ( 𝜒′ ↔ [ 𝑝 / 𝑛 ] 𝜒 )
10		bnj1006.10	⊢ ( 𝜑″ ↔ [ 𝐺 / 𝑓 ] 𝜑′ )
11		bnj1006.11	⊢ ( 𝜓″ ↔ [ 𝐺 / 𝑓 ] 𝜓′ )
12		bnj1006.12	⊢ ( 𝜒″ ↔ [ 𝐺 / 𝑓 ] 𝜒′ )
13		bnj1006.13	⊢ 𝐷 = ( ω ∖ { ∅ } )
14		bnj1006.15	⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 )
15		bnj1006.16	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
16		bnj1006.28	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → ( 𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) )
17	6	simprbi	⊢ ( 𝜂 → 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) )
18	17	bnj708	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) )
19		bnj253	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
20	19	simp1bi	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) → ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) )
21	4 20	sylbi	⊢ ( 𝜃 → ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) )
22	21	bnj705	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) )
23		bnj643	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → 𝜒 )
24		3simpc	⊢ ( ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) → ( 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) )
25	5 24	sylbi	⊢ ( 𝜏 → ( 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) )
26	25	bnj707	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → ( 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) )
27		3anass	⊢ ( ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ↔ ( 𝜒 ∧ ( 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) )
28	23 26 27	sylanbrc	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) )
29		biid	⊢ ( ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
30		biid	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑚 ∈ 𝑛 ) ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑚 ∈ 𝑛 ) )
31	1 2 3 13 14 29 30	bnj969	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝐶 ∈ V )
32	22 28 31	syl2anc	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → 𝐶 ∈ V )
33	3	bnj1235	⊢ ( 𝜒 → 𝑓 Fn 𝑛 )
34	33	bnj706	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → 𝑓 Fn 𝑛 )
35	5	simp3bi	⊢ ( 𝜏 → 𝑝 = suc 𝑛 )
36	35	bnj707	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → 𝑝 = suc 𝑛 )
37	6	simplbi	⊢ ( 𝜂 → 𝑖 ∈ 𝑛 )
38	37	bnj708	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → 𝑖 ∈ 𝑛 )
39	32 34 36 38	bnj951	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑖 ∈ 𝑛 ) )
40	15	bnj945	⊢ ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑖 ∈ 𝑛 ) → ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) )
41	39 40	syl	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) )
42	18 41	eleqtrrd	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) )
43	16	anim1i	⊢ ( ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) → ( ( 𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) )
44		df-bnj17	⊢ ( ( 𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) ↔ ( ( 𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) )
45	43 44	sylibr	⊢ ( ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) → ( 𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) )
46	1 2 3 7 8 9 10 11 12 14 15	bnj999	⊢ ( ( 𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ ( 𝐺 ‘ suc 𝑖 ) )
47	45 46	syl	⊢ ( ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ ( 𝐺 ‘ suc 𝑖 ) )
48	42 47	mpdan	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ ( 𝐺 ‘ suc 𝑖 ) )

Metamath Proof Explorer

Theorem bnj1006

Proof