Metamath Proof Explorer

Theorem 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 𝑛 ∧ 𝜑″ ∧ 𝜓″ ) )