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

Metamath Proof Explorer

Theorem bnj607

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

Proof

Step Hyp Ref Expression
1 bnj607.5 ⊢ ( 𝜃 ↔ ∀ 𝑚 ∈ 𝐷 ( 𝑚 E 𝑛 → [ 𝑚 / 𝑛 ] 𝜒 ) )
2 bnj607.13 ⊢ ( 𝜑″ ↔ [ 𝐺 / 𝑓 ] 𝜑 )
3 bnj607.14 ⊢ ( 𝜓″ ↔ [ 𝐺 / 𝑓 ] 𝜓 )
4 bnj607.17 ⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
5 bnj607.19 ⊢ ( 𝜂 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
6 bnj607.28 ⊢ 𝐺 ∈ V
7 bnj607.31 ⊢ ( 𝜒′ ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) ) )
8 bnj607.32 ⊢ ( 𝜑″ ↔ ( 𝐺 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
9 bnj607.33 ⊢ ( 𝜓″ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
10 bnj607.37 ⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑚 ∃ 𝑝 𝜂 )
11 bnj607.38 ⊢ ( ( 𝜃 ∧ 𝑚 ∈ 𝐷 ∧ 𝑚 E 𝑛 ) → 𝜒′ )
12 bnj607.41 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → 𝐺 Fn 𝑛 )
13 bnj607.42 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → 𝜑″ )
14 bnj607.43 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → 𝜓″ )
15 bnj607.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
16 bnj607.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
17 bnj607.400 ⊢ ( 𝜑0 ↔ [ ℎ / 𝑓 ] 𝜑 )
18 bnj607.401 ⊢ ( 𝜓0 ↔ [ ℎ / 𝑓 ] 𝜓 )
19 bnj607.300 ⊢ ( 𝜑1 ↔ [ 𝐺 / ℎ ] 𝜑0 )
20 bnj607.301 ⊢ ( 𝜓1 ↔ [ 𝐺 / ℎ ] 𝜓0 )
21 10 anim1i ⊢ ( ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) ∧ 𝜃 ) → ( ∃ 𝑚 ∃ 𝑝 𝜂 ∧ 𝜃 ) )
22 nfv ⊢ Ⅎ 𝑝 𝜃
23 22 19.41 ⊢ ( ∃ 𝑝 ( 𝜂 ∧ 𝜃 ) ↔ ( ∃ 𝑝 𝜂 ∧ 𝜃 ) )
24 23 exbii ⊢ ( ∃ 𝑚 ∃ 𝑝 ( 𝜂 ∧ 𝜃 ) ↔ ∃ 𝑚 ( ∃ 𝑝 𝜂 ∧ 𝜃 ) )
25 1 bnj1095 ⊢ ( 𝜃 → ∀ 𝑚 𝜃 )
26 25 nf5i ⊢ Ⅎ 𝑚 𝜃
27 26 19.41 ⊢ ( ∃ 𝑚 ( ∃ 𝑝 𝜂 ∧ 𝜃 ) ↔ ( ∃ 𝑚 ∃ 𝑝 𝜂 ∧ 𝜃 ) )
28 24 27 bitr2i ⊢ ( ( ∃ 𝑚 ∃ 𝑝 𝜂 ∧ 𝜃 ) ↔ ∃ 𝑚 ∃ 𝑝 ( 𝜂 ∧ 𝜃 ) )
29 21 28 sylib ⊢ ( ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) ∧ 𝜃 ) → ∃ 𝑚 ∃ 𝑝 ( 𝜂 ∧ 𝜃 ) )
30 5 bnj1232 ⊢ ( 𝜂 → 𝑚 ∈ 𝐷 )
31 bnj219 ⊢ ( 𝑛 = suc 𝑚 → 𝑚 E 𝑛 )
32 5 31 bnj770 ⊢ ( 𝜂 → 𝑚 E 𝑛 )
33 30 32 jca ⊢ ( 𝜂 → ( 𝑚 ∈ 𝐷 ∧ 𝑚 E 𝑛 ) )
34 33 anim1i ⊢ ( ( 𝜂 ∧ 𝜃 ) → ( ( 𝑚 ∈ 𝐷 ∧ 𝑚 E 𝑛 ) ∧ 𝜃 ) )
35 bnj170 ⊢ ( ( 𝜃 ∧ 𝑚 ∈ 𝐷 ∧ 𝑚 E 𝑛 ) ↔ ( ( 𝑚 ∈ 𝐷 ∧ 𝑚 E 𝑛 ) ∧ 𝜃 ) )
36 34 35 sylibr ⊢ ( ( 𝜂 ∧ 𝜃 ) → ( 𝜃 ∧ 𝑚 ∈ 𝐷 ∧ 𝑚 E 𝑛 ) )
37 36 11 syl ⊢ ( ( 𝜂 ∧ 𝜃 ) → 𝜒′ )
38 simpl ⊢ ( ( 𝜂 ∧ 𝜃 ) → 𝜂 )
39 37 38 jca ⊢ ( ( 𝜂 ∧ 𝜃 ) → ( 𝜒′ ∧ 𝜂 ) )
40 39 2eximi ⊢ ( ∃ 𝑚 ∃ 𝑝 ( 𝜂 ∧ 𝜃 ) → ∃ 𝑚 ∃ 𝑝 ( 𝜒′ ∧ 𝜂 ) )
41 7 biimpi ⊢ ( 𝜒′ → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) ) )
42 euex ⊢ ( ∃! 𝑓 ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) → ∃ 𝑓 ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
43 41 42 syl6 ⊢ ( 𝜒′ → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) ) )
44 43 impcom ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜒′ ) → ∃ 𝑓 ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
45 44 4 bnj1198 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜒′ ) → ∃ 𝑓 𝜏 )
46 45 adantrr ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝜒′ ∧ 𝜂 ) ) → ∃ 𝑓 𝜏 )
47 id ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) )
48 47 3com23 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜂 ∧ 𝜏 ) → ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) )
49 48 3expia ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜂 ) → ( 𝜏 → ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ) )
50 49 eximdv ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜂 ) → ( ∃ 𝑓 𝜏 → ∃ 𝑓 ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ) )
51 50 ad2ant2rl ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝜒′ ∧ 𝜂 ) ) → ( ∃ 𝑓 𝜏 → ∃ 𝑓 ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ) )
52 46 51 mpd ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝜒′ ∧ 𝜂 ) ) → ∃ 𝑓 ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) )
53 12 13 14 3jca ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → ( 𝐺 Fn 𝑛 ∧ 𝜑″ ∧ 𝜓″ ) )
54 53 eximi ⊢ ( ∃ 𝑓 ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → ∃ 𝑓 ( 𝐺 Fn 𝑛 ∧ 𝜑″ ∧ 𝜓″ ) )
55 nfe1 ⊢ Ⅎ 𝑓 ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 )
56 nfcv ⊢ Ⅎ ℎ 𝐺
57 nfv ⊢ Ⅎ ℎ 𝐺 Fn 𝑛
58 nfsbc1v ⊢ Ⅎ ℎ [ 𝐺 / ℎ ] 𝜑0
59 19 58 nfxfr ⊢ Ⅎ ℎ 𝜑1
60 nfsbc1v ⊢ Ⅎ ℎ [ 𝐺 / ℎ ] 𝜓0
61 20 60 nfxfr ⊢ Ⅎ ℎ 𝜓1
62 57 59 61 nf3an ⊢ Ⅎ ℎ ( 𝐺 Fn 𝑛 ∧ 𝜑1 ∧ 𝜓1 )
63 fneq1 ⊢ ( ℎ = 𝐺 → ( ℎ Fn 𝑛 ↔ 𝐺 Fn 𝑛 ) )
64 sbceq1a ⊢ ( ℎ = 𝐺 → ( 𝜑0 ↔ [ 𝐺 / ℎ ] 𝜑0 ) )
65 64 19 bitr4di ⊢ ( ℎ = 𝐺 → ( 𝜑0 ↔ 𝜑1 ) )
66 sbceq1a ⊢ ( ℎ = 𝐺 → ( 𝜓0 ↔ [ 𝐺 / ℎ ] 𝜓0 ) )
67 66 20 bitr4di ⊢ ( ℎ = 𝐺 → ( 𝜓0 ↔ 𝜓1 ) )
68 63 65 67 3anbi123d ⊢ ( ℎ = 𝐺 → ( ( ℎ Fn 𝑛 ∧ 𝜑0 ∧ 𝜓0 ) ↔ ( 𝐺 Fn 𝑛 ∧ 𝜑1 ∧ 𝜓1 ) ) )
69 56 62 68 spcegf ⊢ ( 𝐺 ∈ V → ( ( 𝐺 Fn 𝑛 ∧ 𝜑1 ∧ 𝜓1 ) → ∃ ℎ ( ℎ Fn 𝑛 ∧ 𝜑0 ∧ 𝜓0 ) ) )
70 6 69 ax-mp ⊢ ( ( 𝐺 Fn 𝑛 ∧ 𝜑1 ∧ 𝜓1 ) → ∃ ℎ ( ℎ Fn 𝑛 ∧ 𝜑0 ∧ 𝜓0 ) )
71 17 15 bnj154 ⊢ ( 𝜑0 ↔ ( ℎ ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
72 71 19 6 bnj526 ⊢ ( 𝜑1 ↔ ( 𝐺 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
73 8 72 bitr4i ⊢ ( 𝜑″ ↔ 𝜑1 )
74 vex ⊢ ℎ ∈ V
75 16 18 74 bnj540 ⊢ ( 𝜓0 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( ℎ ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( ℎ ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
76 75 20 6 bnj540 ⊢ ( 𝜓1 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
77 9 76 bitr4i ⊢ ( 𝜓″ ↔ 𝜓1 )
78 73 77 anbi12i ⊢ ( ( 𝜑″ ∧ 𝜓″ ) ↔ ( 𝜑1 ∧ 𝜓1 ) )
79 78 anbi2i ⊢ ( ( 𝐺 Fn 𝑛 ∧ ( 𝜑″ ∧ 𝜓″ ) ) ↔ ( 𝐺 Fn 𝑛 ∧ ( 𝜑1 ∧ 𝜓1 ) ) )
80 3anass ⊢ ( ( 𝐺 Fn 𝑛 ∧ 𝜑″ ∧ 𝜓″ ) ↔ ( 𝐺 Fn 𝑛 ∧ ( 𝜑″ ∧ 𝜓″ ) ) )
81 3anass ⊢ ( ( 𝐺 Fn 𝑛 ∧ 𝜑1 ∧ 𝜓1 ) ↔ ( 𝐺 Fn 𝑛 ∧ ( 𝜑1 ∧ 𝜓1 ) ) )
82 79 80 81 3bitr4i ⊢ ( ( 𝐺 Fn 𝑛 ∧ 𝜑″ ∧ 𝜓″ ) ↔ ( 𝐺 Fn 𝑛 ∧ 𝜑1 ∧ 𝜓1 ) )
83 nfv ⊢ Ⅎ ℎ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 )
84 nfv ⊢ Ⅎ 𝑓 ℎ Fn 𝑛
85 nfsbc1v ⊢ Ⅎ 𝑓 [ ℎ / 𝑓 ] 𝜑
86 17 85 nfxfr ⊢ Ⅎ 𝑓 𝜑0
87 nfsbc1v ⊢ Ⅎ 𝑓 [ ℎ / 𝑓 ] 𝜓
88 18 87 nfxfr ⊢ Ⅎ 𝑓 𝜓0
89 84 86 88 nf3an ⊢ Ⅎ 𝑓 ( ℎ Fn 𝑛 ∧ 𝜑0 ∧ 𝜓0 )
90 fneq1 ⊢ ( 𝑓 = ℎ → ( 𝑓 Fn 𝑛 ↔ ℎ Fn 𝑛 ) )
91 sbceq1a ⊢ ( 𝑓 = ℎ → ( 𝜑 ↔ [ ℎ / 𝑓 ] 𝜑 ) )
92 91 17 bitr4di ⊢ ( 𝑓 = ℎ → ( 𝜑 ↔ 𝜑0 ) )
93 sbceq1a ⊢ ( 𝑓 = ℎ → ( 𝜓 ↔ [ ℎ / 𝑓 ] 𝜓 ) )
94 93 18 bitr4di ⊢ ( 𝑓 = ℎ → ( 𝜓 ↔ 𝜓0 ) )
95 90 92 94 3anbi123d ⊢ ( 𝑓 = ℎ → ( ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ( ℎ Fn 𝑛 ∧ 𝜑0 ∧ 𝜓0 ) ) )
96 83 89 95 cbvexv1 ⊢ ( ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ∃ ℎ ( ℎ Fn 𝑛 ∧ 𝜑0 ∧ 𝜓0 ) )
97 70 82 96 3imtr4i ⊢ ( ( 𝐺 Fn 𝑛 ∧ 𝜑″ ∧ 𝜓″ ) → ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
98 55 97 exlimi ⊢ ( ∃ 𝑓 ( 𝐺 Fn 𝑛 ∧ 𝜑″ ∧ 𝜓″ ) → ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
99 52 54 98 3syl ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝜒′ ∧ 𝜂 ) ) → ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
100 99 expcom ⊢ ( ( 𝜒′ ∧ 𝜂 ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
101 100 exlimivv ⊢ ( ∃ 𝑚 ∃ 𝑝 ( 𝜒′ ∧ 𝜂 ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
102 29 40 101 3syl ⊢ ( ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) ∧ 𝜃 ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
103 102 3impa ⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ∧ 𝜃 ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )