This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj605

Description: Technical lemma. 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 bnj605.5 ⊢ ( 𝜃 ↔ ∀ 𝑚 ∈ 𝐷 ( 𝑚 E 𝑛 → [ 𝑚 / 𝑛 ] 𝜒 ) )
bnj605.13 ⊢ ( 𝜑″ ↔ [ 𝑓 / 𝑓 ] 𝜑 )
bnj605.14 ⊢ ( 𝜓″ ↔ [ 𝑓 / 𝑓 ] 𝜓 )
bnj605.17 ⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
bnj605.19 ⊢ ( 𝜂 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
bnj605.28 ⊢ 𝑓 ∈ V
bnj605.31 ⊢ ( 𝜒′ ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) ) )
bnj605.32 ⊢ ( 𝜑″ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
bnj605.33 ⊢ ( 𝜓″ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
bnj605.37 ⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑚 ∃ 𝑝 𝜂 )
bnj605.38 ⊢ ( ( 𝜃 ∧ 𝑚 ∈ 𝐷 ∧ 𝑚 E 𝑛 ) → 𝜒′ )
bnj605.41 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → 𝑓 Fn 𝑛 )
bnj605.42 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → 𝜑″ )
bnj605.43 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → 𝜓″ )
Assertion bnj605 ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ∧ 𝜃 ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 bnj605.5 ⊢ ( 𝜃 ↔ ∀ 𝑚 ∈ 𝐷 ( 𝑚 E 𝑛 → [ 𝑚 / 𝑛 ] 𝜒 ) )
2 bnj605.13 ⊢ ( 𝜑″ ↔ [ 𝑓 / 𝑓 ] 𝜑 )
3 bnj605.14 ⊢ ( 𝜓″ ↔ [ 𝑓 / 𝑓 ] 𝜓 )
4 bnj605.17 ⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
5 bnj605.19 ⊢ ( 𝜂 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
6 bnj605.28 ⊢ 𝑓 ∈ V
7 bnj605.31 ⊢ ( 𝜒′ ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) ) )
8 bnj605.32 ⊢ ( 𝜑″ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
9 bnj605.33 ⊢ ( 𝜓″ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
10 bnj605.37 ⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑚 ∃ 𝑝 𝜂 )
11 bnj605.38 ⊢ ( ( 𝜃 ∧ 𝑚 ∈ 𝐷 ∧ 𝑚 E 𝑛 ) → 𝜒′ )
12 bnj605.41 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → 𝑓 Fn 𝑛 )
13 bnj605.42 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → 𝜑″ )
14 bnj605.43 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → 𝜓″ )
15 10 anim1i ⊢ ( ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) ∧ 𝜃 ) → ( ∃ 𝑚 ∃ 𝑝 𝜂 ∧ 𝜃 ) )
16 nfv ⊢ Ⅎ 𝑝 𝜃
17 16 19.41 ⊢ ( ∃ 𝑝 ( 𝜂 ∧ 𝜃 ) ↔ ( ∃ 𝑝 𝜂 ∧ 𝜃 ) )
18 17 exbii ⊢ ( ∃ 𝑚 ∃ 𝑝 ( 𝜂 ∧ 𝜃 ) ↔ ∃ 𝑚 ( ∃ 𝑝 𝜂 ∧ 𝜃 ) )
19 1 bnj1095 ⊢ ( 𝜃 → ∀ 𝑚 𝜃 )
20 19 nf5i ⊢ Ⅎ 𝑚 𝜃
21 20 19.41 ⊢ ( ∃ 𝑚 ( ∃ 𝑝 𝜂 ∧ 𝜃 ) ↔ ( ∃ 𝑚 ∃ 𝑝 𝜂 ∧ 𝜃 ) )
22 18 21 bitr2i ⊢ ( ( ∃ 𝑚 ∃ 𝑝 𝜂 ∧ 𝜃 ) ↔ ∃ 𝑚 ∃ 𝑝 ( 𝜂 ∧ 𝜃 ) )
23 15 22 sylib ⊢ ( ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) ∧ 𝜃 ) → ∃ 𝑚 ∃ 𝑝 ( 𝜂 ∧ 𝜃 ) )
24 5 bnj1232 ⊢ ( 𝜂 → 𝑚 ∈ 𝐷 )
25 bnj219 ⊢ ( 𝑛 = suc 𝑚 → 𝑚 E 𝑛 )
26 5 25 bnj770 ⊢ ( 𝜂 → 𝑚 E 𝑛 )
27 24 26 jca ⊢ ( 𝜂 → ( 𝑚 ∈ 𝐷 ∧ 𝑚 E 𝑛 ) )
28 27 anim1i ⊢ ( ( 𝜂 ∧ 𝜃 ) → ( ( 𝑚 ∈ 𝐷 ∧ 𝑚 E 𝑛 ) ∧ 𝜃 ) )
29 bnj170 ⊢ ( ( 𝜃 ∧ 𝑚 ∈ 𝐷 ∧ 𝑚 E 𝑛 ) ↔ ( ( 𝑚 ∈ 𝐷 ∧ 𝑚 E 𝑛 ) ∧ 𝜃 ) )
30 28 29 sylibr ⊢ ( ( 𝜂 ∧ 𝜃 ) → ( 𝜃 ∧ 𝑚 ∈ 𝐷 ∧ 𝑚 E 𝑛 ) )
31 30 11 syl ⊢ ( ( 𝜂 ∧ 𝜃 ) → 𝜒′ )
32 simpl ⊢ ( ( 𝜂 ∧ 𝜃 ) → 𝜂 )
33 31 32 jca ⊢ ( ( 𝜂 ∧ 𝜃 ) → ( 𝜒′ ∧ 𝜂 ) )
34 33 2eximi ⊢ ( ∃ 𝑚 ∃ 𝑝 ( 𝜂 ∧ 𝜃 ) → ∃ 𝑚 ∃ 𝑝 ( 𝜒′ ∧ 𝜂 ) )
35 bnj248 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂 ) ↔ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜒′ ) ∧ 𝜂 ) )
36 pm3.35 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) ) ) → ∃! 𝑓 ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
37 7 36 sylan2b ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜒′ ) → ∃! 𝑓 ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
38 euex ⊢ ( ∃! 𝑓 ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) → ∃ 𝑓 ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
39 37 38 syl ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜒′ ) → ∃ 𝑓 ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
40 39 4 bnj1198 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜒′ ) → ∃ 𝑓 𝜏 )
41 35 40 bnj832 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂 ) → ∃ 𝑓 𝜏 )
42 12 13 14 3jca ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → ( 𝑓 Fn 𝑛 ∧ 𝜑″ ∧ 𝜓″ ) )
43 42 3com23 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜂 ∧ 𝜏 ) → ( 𝑓 Fn 𝑛 ∧ 𝜑″ ∧ 𝜓″ ) )
44 43 3expia ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜂 ) → ( 𝜏 → ( 𝑓 Fn 𝑛 ∧ 𝜑″ ∧ 𝜓″ ) ) )
45 44 eximdv ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜂 ) → ( ∃ 𝑓 𝜏 → ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑″ ∧ 𝜓″ ) ) )
46 45 ad4ant14 ⊢ ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜒′ ) ∧ 𝜂 ) → ( ∃ 𝑓 𝜏 → ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑″ ∧ 𝜓″ ) ) )
47 35 46 sylbi ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂 ) → ( ∃ 𝑓 𝜏 → ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑″ ∧ 𝜓″ ) ) )
48 41 47 mpd ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂 ) → ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑″ ∧ 𝜓″ ) )
49 bnj432 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂 ) ↔ ( ( 𝜒′ ∧ 𝜂 ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) )
50 biid ⊢ ( 𝑓 Fn 𝑛 ↔ 𝑓 Fn 𝑛 )
51 sbcid ⊢ ( [ 𝑓 / 𝑓 ] 𝜑 ↔ 𝜑 )
52 2 51 bitri ⊢ ( 𝜑″ ↔ 𝜑 )
53 sbcid ⊢ ( [ 𝑓 / 𝑓 ] 𝜓 ↔ 𝜓 )
54 3 53 bitri ⊢ ( 𝜓″ ↔ 𝜓 )
55 50 52 54 3anbi123i ⊢ ( ( 𝑓 Fn 𝑛 ∧ 𝜑″ ∧ 𝜓″ ) ↔ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
56 55 exbii ⊢ ( ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑″ ∧ 𝜓″ ) ↔ ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
57 48 49 56 3imtr3i ⊢ ( ( ( 𝜒′ ∧ 𝜂 ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
58 57 ex ⊢ ( ( 𝜒′ ∧ 𝜂 ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
59 58 exlimivv ⊢ ( ∃ 𝑚 ∃ 𝑝 ( 𝜒′ ∧ 𝜂 ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
60 23 34 59 3syl ⊢ ( ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) ∧ 𝜃 ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
61 60 3impa ⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ∧ 𝜃 ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )