Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj607 Structured version   Visualization version   GIF version

Theorem bnj607 32087
Description: Technical lemma for bnj852 32092. 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.)
Hypotheses
Ref Expression
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
Ref Expression
bnj607 ((𝑛 ≠ 1o𝑛𝐷𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
Distinct variable groups:   𝐴,𝑓,   𝐴,𝑚,𝑓   𝐴,𝑝,𝑓   ,𝐺,𝑖,𝑦   𝑅,𝑓,   𝑅,𝑚   𝑅,𝑝   𝜂,𝑓   𝑓,𝑖,𝑦   𝑓,𝑛,   𝑥,𝑓,   𝜑,   𝜓,   𝑚,𝑛   𝜑,𝑚   𝜓,𝑚   𝑥,𝑚   𝑛,𝑝   𝜑,𝑝   𝜓,𝑝   𝜃,𝑝   𝑥,𝑝
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑓,𝑖,𝑛)   𝜓(𝑥,𝑦,𝑓,𝑖,𝑛)   𝜒(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜃(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛)   𝜏(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜂(𝑥,𝑦,,𝑖,𝑚,𝑛,𝑝)   𝐴(𝑥,𝑦,𝑖,𝑛)   𝐷(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝑅(𝑥,𝑦,𝑖,𝑛)   𝐺(𝑥,𝑓,𝑚,𝑛,𝑝)   𝜑′(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜓′(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜒′(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜑″(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜓″(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜑0(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜓0(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜑1(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜓1(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)

Proof of Theorem bnj607
StepHypRef Expression
1 bnj607.37 . . . . 5 ((𝑛 ≠ 1o𝑛𝐷) → ∃𝑚𝑝𝜂)
21anim1i 614 . . . 4 (((𝑛 ≠ 1o𝑛𝐷) ∧ 𝜃) → (∃𝑚𝑝𝜂𝜃))
3 nfv 1906 . . . . . . 7 𝑝𝜃
4319.41 2227 . . . . . 6 (∃𝑝(𝜂𝜃) ↔ (∃𝑝𝜂𝜃))
54exbii 1839 . . . . 5 (∃𝑚𝑝(𝜂𝜃) ↔ ∃𝑚(∃𝑝𝜂𝜃))
6 bnj607.5 . . . . . . . 8 (𝜃 ↔ ∀𝑚𝐷 (𝑚 E 𝑛[𝑚 / 𝑛]𝜒))
76bnj1095 31952 . . . . . . 7 (𝜃 → ∀𝑚𝜃)
87nf5i 2141 . . . . . 6 𝑚𝜃
9819.41 2227 . . . . 5 (∃𝑚(∃𝑝𝜂𝜃) ↔ (∃𝑚𝑝𝜂𝜃))
105, 9bitr2i 277 . . . 4 ((∃𝑚𝑝𝜂𝜃) ↔ ∃𝑚𝑝(𝜂𝜃))
112, 10sylib 219 . . 3 (((𝑛 ≠ 1o𝑛𝐷) ∧ 𝜃) → ∃𝑚𝑝(𝜂𝜃))
12 bnj607.19 . . . . . . . . . 10 (𝜂 ↔ (𝑚𝐷𝑛 = suc 𝑚𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))
1312bnj1232 31974 . . . . . . . . 9 (𝜂𝑚𝐷)
14 bnj219 31902 . . . . . . . . . 10 (𝑛 = suc 𝑚𝑚 E 𝑛)
1512, 14bnj770 31933 . . . . . . . . 9 (𝜂𝑚 E 𝑛)
1613, 15jca 512 . . . . . . . 8 (𝜂 → (𝑚𝐷𝑚 E 𝑛))
1716anim1i 614 . . . . . . 7 ((𝜂𝜃) → ((𝑚𝐷𝑚 E 𝑛) ∧ 𝜃))
18 bnj170 31867 . . . . . . 7 ((𝜃𝑚𝐷𝑚 E 𝑛) ↔ ((𝑚𝐷𝑚 E 𝑛) ∧ 𝜃))
1917, 18sylibr 235 . . . . . 6 ((𝜂𝜃) → (𝜃𝑚𝐷𝑚 E 𝑛))
20 bnj607.38 . . . . . 6 ((𝜃𝑚𝐷𝑚 E 𝑛) → 𝜒′)
2119, 20syl 17 . . . . 5 ((𝜂𝜃) → 𝜒′)
22 simpl 483 . . . . 5 ((𝜂𝜃) → 𝜂)
2321, 22jca 512 . . . 4 ((𝜂𝜃) → (𝜒′𝜂))
24232eximi 1827 . . 3 (∃𝑚𝑝(𝜂𝜃) → ∃𝑚𝑝(𝜒′𝜂))
25 bnj607.31 . . . . . . . . . . . 12 (𝜒′ ↔ ((𝑅 FrSe 𝐴𝑥𝐴) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′)))
2625biimpi 217 . . . . . . . . . . 11 (𝜒′ → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′)))
27 euex 2655 . . . . . . . . . . 11 (∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
2826, 27syl6 35 . . . . . . . . . 10 (𝜒′ → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′)))
2928impcom 408 . . . . . . . . 9 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
30 bnj607.17 . . . . . . . . 9 (𝜏 ↔ (𝑓 Fn 𝑚𝜑′𝜓′))
3129, 30bnj1198 31966 . . . . . . . 8 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃𝑓𝜏)
3231adantrr 713 . . . . . . 7 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ (𝜒′𝜂)) → ∃𝑓𝜏)
33 id 22 . . . . . . . . . . 11 ((𝑅 FrSe 𝐴𝜏𝜂) → (𝑅 FrSe 𝐴𝜏𝜂))
34333com23 1118 . . . . . . . . . 10 ((𝑅 FrSe 𝐴𝜂𝜏) → (𝑅 FrSe 𝐴𝜏𝜂))
35343expia 1113 . . . . . . . . 9 ((𝑅 FrSe 𝐴𝜂) → (𝜏 → (𝑅 FrSe 𝐴𝜏𝜂)))
3635eximdv 1909 . . . . . . . 8 ((𝑅 FrSe 𝐴𝜂) → (∃𝑓𝜏 → ∃𝑓(𝑅 FrSe 𝐴𝜏𝜂)))
3736ad2ant2rl 745 . . . . . . 7 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ (𝜒′𝜂)) → (∃𝑓𝜏 → ∃𝑓(𝑅 FrSe 𝐴𝜏𝜂)))
3832, 37mpd 15 . . . . . 6 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ (𝜒′𝜂)) → ∃𝑓(𝑅 FrSe 𝐴𝜏𝜂))
39 bnj607.41 . . . . . . . 8 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝐺 Fn 𝑛)
40 bnj607.42 . . . . . . . 8 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝜑″)
41 bnj607.43 . . . . . . . 8 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝜓″)
4239, 40, 413jca 1120 . . . . . . 7 ((𝑅 FrSe 𝐴𝜏𝜂) → (𝐺 Fn 𝑛𝜑″𝜓″))
4342eximi 1826 . . . . . 6 (∃𝑓(𝑅 FrSe 𝐴𝜏𝜂) → ∃𝑓(𝐺 Fn 𝑛𝜑″𝜓″))
44 nfe1 2145 . . . . . . 7 𝑓𝑓(𝑓 Fn 𝑛𝜑𝜓)
45 bnj607.28 . . . . . . . . 9 𝐺 ∈ V
46 nfcv 2974 . . . . . . . . . 10 𝐺
47 nfv 1906 . . . . . . . . . . 11 𝐺 Fn 𝑛
48 bnj607.300 . . . . . . . . . . . 12 (𝜑1[𝐺 / ]𝜑0)
49 nfsbc1v 3789 . . . . . . . . . . . 12 [𝐺 / ]𝜑0
5048, 49nfxfr 1844 . . . . . . . . . . 11 𝜑1
51 bnj607.301 . . . . . . . . . . . 12 (𝜓1[𝐺 / ]𝜓0)
52 nfsbc1v 3789 . . . . . . . . . . . 12 [𝐺 / ]𝜓0
5351, 52nfxfr 1844 . . . . . . . . . . 11 𝜓1
5447, 50, 53nf3an 1893 . . . . . . . . . 10 (𝐺 Fn 𝑛𝜑1𝜓1)
55 fneq1 6437 . . . . . . . . . . 11 ( = 𝐺 → ( Fn 𝑛𝐺 Fn 𝑛))
56 sbceq1a 3780 . . . . . . . . . . . 12 ( = 𝐺 → (𝜑0[𝐺 / ]𝜑0))
5756, 48syl6bbr 290 . . . . . . . . . . 11 ( = 𝐺 → (𝜑0𝜑1))
58 sbceq1a 3780 . . . . . . . . . . . 12 ( = 𝐺 → (𝜓0[𝐺 / ]𝜓0))
5958, 51syl6bbr 290 . . . . . . . . . . 11 ( = 𝐺 → (𝜓0𝜓1))
6055, 57, 593anbi123d 1427 . . . . . . . . . 10 ( = 𝐺 → (( Fn 𝑛𝜑0𝜓0) ↔ (𝐺 Fn 𝑛𝜑1𝜓1)))
6146, 54, 60spcegf 3588 . . . . . . . . 9 (𝐺 ∈ V → ((𝐺 Fn 𝑛𝜑1𝜓1) → ∃( Fn 𝑛𝜑0𝜓0)))
6245, 61ax-mp 5 . . . . . . . 8 ((𝐺 Fn 𝑛𝜑1𝜓1) → ∃( Fn 𝑛𝜑0𝜓0))
63 bnj607.32 . . . . . . . . . . . 12 (𝜑″ ↔ (𝐺‘∅) = pred(𝑥, 𝐴, 𝑅))
64 bnj607.400 . . . . . . . . . . . . . 14 (𝜑0[ / 𝑓]𝜑)
65 bnj607.1 . . . . . . . . . . . . . 14 (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
6664, 65bnj154 32049 . . . . . . . . . . . . 13 (𝜑0 ↔ (‘∅) = pred(𝑥, 𝐴, 𝑅))
6766, 48, 45bnj526 32059 . . . . . . . . . . . 12 (𝜑1 ↔ (𝐺‘∅) = pred(𝑥, 𝐴, 𝑅))
6863, 67bitr4i 279 . . . . . . . . . . 11 (𝜑″𝜑1)
69 bnj607.33 . . . . . . . . . . . 12 (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝐺‘suc 𝑖) = 𝑦 ∈ (𝐺𝑖) pred(𝑦, 𝐴, 𝑅)))
70 bnj607.2 . . . . . . . . . . . . . 14 (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))
71 bnj607.401 . . . . . . . . . . . . . 14 (𝜓0[ / 𝑓]𝜓)
72 vex 3495 . . . . . . . . . . . . . 14 ∈ V
7370, 71, 72bnj540 32063 . . . . . . . . . . . . 13 (𝜓0 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (‘suc 𝑖) = 𝑦 ∈ (𝑖) pred(𝑦, 𝐴, 𝑅)))
7473, 51, 45bnj540 32063 . . . . . . . . . . . 12 (𝜓1 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝐺‘suc 𝑖) = 𝑦 ∈ (𝐺𝑖) pred(𝑦, 𝐴, 𝑅)))
7569, 74bitr4i 279 . . . . . . . . . . 11 (𝜓″𝜓1)
7668, 75anbi12i 626 . . . . . . . . . 10 ((𝜑″𝜓″) ↔ (𝜑1𝜓1))
7776anbi2i 622 . . . . . . . . 9 ((𝐺 Fn 𝑛 ∧ (𝜑″𝜓″)) ↔ (𝐺 Fn 𝑛 ∧ (𝜑1𝜓1)))
78 3anass 1087 . . . . . . . . 9 ((𝐺 Fn 𝑛𝜑″𝜓″) ↔ (𝐺 Fn 𝑛 ∧ (𝜑″𝜓″)))
79 3anass 1087 . . . . . . . . 9 ((𝐺 Fn 𝑛𝜑1𝜓1) ↔ (𝐺 Fn 𝑛 ∧ (𝜑1𝜓1)))
8077, 78, 793bitr4i 304 . . . . . . . 8 ((𝐺 Fn 𝑛𝜑″𝜓″) ↔ (𝐺 Fn 𝑛𝜑1𝜓1))
81 nfv 1906 . . . . . . . . 9 (𝑓 Fn 𝑛𝜑𝜓)
82 nfv 1906 . . . . . . . . . 10 𝑓 Fn 𝑛
83 nfsbc1v 3789 . . . . . . . . . . 11 𝑓[ / 𝑓]𝜑
8464, 83nfxfr 1844 . . . . . . . . . 10 𝑓𝜑0
85 nfsbc1v 3789 . . . . . . . . . . 11 𝑓[ / 𝑓]𝜓
8671, 85nfxfr 1844 . . . . . . . . . 10 𝑓𝜓0
8782, 84, 86nf3an 1893 . . . . . . . . 9 𝑓( Fn 𝑛𝜑0𝜓0)
88 fneq1 6437 . . . . . . . . . 10 (𝑓 = → (𝑓 Fn 𝑛 Fn 𝑛))
89 sbceq1a 3780 . . . . . . . . . . 11 (𝑓 = → (𝜑[ / 𝑓]𝜑))
9089, 64syl6bbr 290 . . . . . . . . . 10 (𝑓 = → (𝜑𝜑0))
91 sbceq1a 3780 . . . . . . . . . . 11 (𝑓 = → (𝜓[ / 𝑓]𝜓))
9291, 71syl6bbr 290 . . . . . . . . . 10 (𝑓 = → (𝜓𝜓0))
9388, 90, 923anbi123d 1427 . . . . . . . . 9 (𝑓 = → ((𝑓 Fn 𝑛𝜑𝜓) ↔ ( Fn 𝑛𝜑0𝜓0)))
9481, 87, 93cbvexv1 2353 . . . . . . . 8 (∃𝑓(𝑓 Fn 𝑛𝜑𝜓) ↔ ∃( Fn 𝑛𝜑0𝜓0))
9562, 80, 943imtr4i 293 . . . . . . 7 ((𝐺 Fn 𝑛𝜑″𝜓″) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
9644, 95exlimi 2207 . . . . . 6 (∃𝑓(𝐺 Fn 𝑛𝜑″𝜓″) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
9738, 43, 963syl 18 . . . . 5 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ (𝜒′𝜂)) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
9897expcom 414 . . . 4 ((𝜒′𝜂) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
9998exlimivv 1924 . . 3 (∃𝑚𝑝(𝜒′𝜂) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
10011, 24, 993syl 18 . 2 (((𝑛 ≠ 1o𝑛𝐷) ∧ 𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
1011003impa 1102 1 ((𝑛 ≠ 1o𝑛𝐷𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wex 1771  wcel 2105  ∃!weu 2646  wne 3013  wral 3135  Vcvv 3492  [wsbc 3769  c0 4288   ciun 4910   class class class wbr 5057   E cep 5457  suc csuc 6186   Fn wfn 6343  cfv 6348  ωcom 7569  1oc1o 8084  w-bnj17 31855   predc-bnj14 31857   FrSe w-bnj15 31861
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-eprel 5458  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-fv 6356  df-bnj17 31856
This theorem is referenced by:  bnj600  32090
  Copyright terms: Public domain W3C validator