bnj908

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	bnj908.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
	bnj908.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj908.3	⊢ 𝐷 = ( ω ∖ { ∅ } )
	bnj908.4	⊢ ( 𝜒 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
	bnj908.5	⊢ ( 𝜃 ↔ ∀ 𝑚 ∈ 𝐷 ( 𝑚 E 𝑛 → [ 𝑚 / 𝑛 ] 𝜒 ) )
	bnj908.10	⊢ ( 𝜑′ ↔ [ 𝑚 / 𝑛 ] 𝜑 )
	bnj908.11	⊢ ( 𝜓′ ↔ [ 𝑚 / 𝑛 ] 𝜓 )
	bnj908.12	⊢ ( 𝜒′ ↔ [ 𝑚 / 𝑛 ] 𝜒 )
	bnj908.13	⊢ ( 𝜑″ ↔ [ 𝐺 / 𝑓 ] 𝜑 )
	bnj908.14	⊢ ( 𝜓″ ↔ [ 𝐺 / 𝑓 ] 𝜓 )
	bnj908.15	⊢ ( 𝜒″ ↔ [ 𝐺 / 𝑓 ] 𝜒 )
	bnj908.16	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } )
	bnj908.17	⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
	bnj908.18	⊢ ( 𝜎 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) )
	bnj908.19	⊢ ( 𝜂 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
	bnj908.20	⊢ ( 𝜁 ↔ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖 ) )
	bnj908.21	⊢ ( 𝜌 ↔ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖 ) )
	bnj908.22	⊢ 𝐵 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
	bnj908.23	⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
	bnj908.24	⊢ 𝐾 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
	bnj908.25	⊢ 𝐿 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
	bnj908.26	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , 𝐶 ⟩ } )
Assertion	bnj908	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂 ) → ∃ 𝑓 ( 𝐺 Fn 𝑛 ∧ 𝜑″ ∧ 𝜓″ ) )

Proof

Step	Hyp	Ref	Expression
1		bnj908.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
2		bnj908.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3		bnj908.3	⊢ 𝐷 = ( ω ∖ { ∅ } )
4		bnj908.4	⊢ ( 𝜒 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
5		bnj908.5	⊢ ( 𝜃 ↔ ∀ 𝑚 ∈ 𝐷 ( 𝑚 E 𝑛 → [ 𝑚 / 𝑛 ] 𝜒 ) )
6		bnj908.10	⊢ ( 𝜑′ ↔ [ 𝑚 / 𝑛 ] 𝜑 )
7		bnj908.11	⊢ ( 𝜓′ ↔ [ 𝑚 / 𝑛 ] 𝜓 )
8		bnj908.12	⊢ ( 𝜒′ ↔ [ 𝑚 / 𝑛 ] 𝜒 )
9		bnj908.13	⊢ ( 𝜑″ ↔ [ 𝐺 / 𝑓 ] 𝜑 )
10		bnj908.14	⊢ ( 𝜓″ ↔ [ 𝐺 / 𝑓 ] 𝜓 )
11		bnj908.15	⊢ ( 𝜒″ ↔ [ 𝐺 / 𝑓 ] 𝜒 )
12		bnj908.16	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } )
13		bnj908.17	⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
14		bnj908.18	⊢ ( 𝜎 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) )
15		bnj908.19	⊢ ( 𝜂 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
16		bnj908.20	⊢ ( 𝜁 ↔ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖 ) )
17		bnj908.21	⊢ ( 𝜌 ↔ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖 ) )
18		bnj908.22	⊢ 𝐵 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
19		bnj908.23	⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
20		bnj908.24	⊢ 𝐾 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
21		bnj908.25	⊢ 𝐿 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
22		bnj908.26	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , 𝐶 ⟩ } )
23		bnj248	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂 ) ↔ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜒′ ) ∧ 𝜂 ) )
24		vex	⊢ 𝑚 ∈ V
25	4 6 7 8 24	bnj207	⊢ ( 𝜒′ ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) ) )
26	25	biimpi	⊢ ( 𝜒′ → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) ) )
27		euex	⊢ ( ∃! 𝑓 ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) → ∃ 𝑓 ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
28	26 27	syl6	⊢ ( 𝜒′ → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) ) )
29	28	impcom	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜒′ ) → ∃ 𝑓 ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
30	29 13	bnj1198	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜒′ ) → ∃ 𝑓 𝜏 )
31	23 30	bnj832	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂 ) → ∃ 𝑓 𝜏 )
32		bnj645	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂 ) → 𝜂 )
33		19.41v	⊢ ( ∃ 𝑓 ( 𝜏 ∧ 𝜂 ) ↔ ( ∃ 𝑓 𝜏 ∧ 𝜂 ) )
34	31 32 33	sylanbrc	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂 ) → ∃ 𝑓 ( 𝜏 ∧ 𝜂 ) )
35		bnj642	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂 ) → 𝑅 FrSe 𝐴 )
36		19.41v	⊢ ( ∃ 𝑓 ( ( 𝜏 ∧ 𝜂 ) ∧ 𝑅 FrSe 𝐴 ) ↔ ( ∃ 𝑓 ( 𝜏 ∧ 𝜂 ) ∧ 𝑅 FrSe 𝐴 ) )
37	34 35 36	sylanbrc	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂 ) → ∃ 𝑓 ( ( 𝜏 ∧ 𝜂 ) ∧ 𝑅 FrSe 𝐴 ) )
38		bnj170	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ↔ ( ( 𝜏 ∧ 𝜂 ) ∧ 𝑅 FrSe 𝐴 ) )
39	37 38	bnj1198	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂 ) → ∃ 𝑓 ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) )
40	1 6 24	bnj523	⊢ ( 𝜑′ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
41	2 7 24	bnj539	⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑚 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
42	40 41 3 12 13 14	bnj544	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → 𝐺 Fn 𝑛 )
43	14 15 42	bnj561	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → 𝐺 Fn 𝑛 )
44	12	bnj528	⊢ 𝐺 ∈ V
45	1 9 44	bnj609	⊢ ( 𝜑″ ↔ ( 𝐺 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
46	40 3 12 13 14 42 45	bnj545	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → 𝜑″ )
47	14 15 46	bnj562	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → 𝜑″ )
48	2 10 44	bnj611	⊢ ( 𝜓″ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
49	3 12 13 14 15 16 18 19 20 21 22 40 41 42 17 43 48	bnj571	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → 𝜓″ )
50	43 47 49	3jca	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → ( 𝐺 Fn 𝑛 ∧ 𝜑″ ∧ 𝜓″ ) )
51	39 50	bnj593	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂 ) → ∃ 𝑓 ( 𝐺 Fn 𝑛 ∧ 𝜑″ ∧ 𝜓″ ) )

Metamath Proof Explorer

Theorem bnj908

Proof