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

Proof of Theorem bnj607
StepHypRef Expression
1 bnj607.37 . . . . 5 ((𝑛 ≠ 1𝑜𝑛𝐷) → ∃𝑚𝑝𝜂)
21anim1i 604 . . . 4 (((𝑛 ≠ 1𝑜𝑛𝐷) ∧ 𝜃) → (∃𝑚𝑝𝜂𝜃))
3 nfv 2005 . . . . . . 7 𝑝𝜃
4319.41 2271 . . . . . 6 (∃𝑝(𝜂𝜃) ↔ (∃𝑝𝜂𝜃))
54exbii 1933 . . . . 5 (∃𝑚𝑝(𝜂𝜃) ↔ ∃𝑚(∃𝑝𝜂𝜃))
6 bnj607.5 . . . . . . . 8 (𝜃 ↔ ∀𝑚𝐷 (𝑚 E 𝑛[𝑚 / 𝑛]𝜒))
76bnj1095 31170 . . . . . . 7 (𝜃 → ∀𝑚𝜃)
87nf5i 2190 . . . . . 6 𝑚𝜃
9819.41 2271 . . . . 5 (∃𝑚(∃𝑝𝜂𝜃) ↔ (∃𝑚𝑝𝜂𝜃))
105, 9bitr2i 267 . . . 4 ((∃𝑚𝑝𝜂𝜃) ↔ ∃𝑚𝑝(𝜂𝜃))
112, 10sylib 209 . . 3 (((𝑛 ≠ 1𝑜𝑛𝐷) ∧ 𝜃) → ∃𝑚𝑝(𝜂𝜃))
12 bnj607.19 . . . . . . . . . 10 (𝜂 ↔ (𝑚𝐷𝑛 = suc 𝑚𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))
1312bnj1232 31192 . . . . . . . . 9 (𝜂𝑚𝐷)
14 bnj219 31120 . . . . . . . . . 10 (𝑛 = suc 𝑚𝑚 E 𝑛)
1512, 14bnj770 31151 . . . . . . . . 9 (𝜂𝑚 E 𝑛)
1613, 15jca 503 . . . . . . . 8 (𝜂 → (𝑚𝐷𝑚 E 𝑛))
1716anim1i 604 . . . . . . 7 ((𝜂𝜃) → ((𝑚𝐷𝑚 E 𝑛) ∧ 𝜃))
18 bnj170 31085 . . . . . . 7 ((𝜃𝑚𝐷𝑚 E 𝑛) ↔ ((𝑚𝐷𝑚 E 𝑛) ∧ 𝜃))
1917, 18sylibr 225 . . . . . 6 ((𝜂𝜃) → (𝜃𝑚𝐷𝑚 E 𝑛))
20 bnj607.38 . . . . . 6 ((𝜃𝑚𝐷𝑚 E 𝑛) → 𝜒′)
2119, 20syl 17 . . . . 5 ((𝜂𝜃) → 𝜒′)
22 simpl 470 . . . . 5 ((𝜂𝜃) → 𝜂)
2321, 22jca 503 . . . 4 ((𝜂𝜃) → (𝜒′𝜂))
24232eximi 1920 . . 3 (∃𝑚𝑝(𝜂𝜃) → ∃𝑚𝑝(𝜒′𝜂))
25 bnj607.31 . . . . . . . . . . . 12 (𝜒′ ↔ ((𝑅 FrSe 𝐴𝑥𝐴) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′)))
2625biimpi 207 . . . . . . . . . . 11 (𝜒′ → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′)))
27 euex 2656 . . . . . . . . . . 11 (∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
2826, 27syl6 35 . . . . . . . . . 10 (𝜒′ → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′)))
2928impcom 396 . . . . . . . . 9 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
30 bnj607.17 . . . . . . . . 9 (𝜏 ↔ (𝑓 Fn 𝑚𝜑′𝜓′))
3129, 30bnj1198 31184 . . . . . . . 8 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃𝑓𝜏)
3231adantrr 699 . . . . . . 7 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ (𝜒′𝜂)) → ∃𝑓𝜏)
33 id 22 . . . . . . . . . . 11 ((𝑅 FrSe 𝐴𝜏𝜂) → (𝑅 FrSe 𝐴𝜏𝜂))
34333com23 1149 . . . . . . . . . 10 ((𝑅 FrSe 𝐴𝜂𝜏) → (𝑅 FrSe 𝐴𝜏𝜂))
35343expia 1143 . . . . . . . . 9 ((𝑅 FrSe 𝐴𝜂) → (𝜏 → (𝑅 FrSe 𝐴𝜏𝜂)))
3635eximdv 2008 . . . . . . . 8 ((𝑅 FrSe 𝐴𝜂) → (∃𝑓𝜏 → ∃𝑓(𝑅 FrSe 𝐴𝜏𝜂)))
3736ad2ant2rl 746 . . . . . . 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 1151 . . . . . . 7 ((𝑅 FrSe 𝐴𝜏𝜂) → (𝐺 Fn 𝑛𝜑″𝜓″))
4342eximi 1919 . . . . . 6 (∃𝑓(𝑅 FrSe 𝐴𝜏𝜂) → ∃𝑓(𝐺 Fn 𝑛𝜑″𝜓″))
44 nfe1 2194 . . . . . . 7 𝑓𝑓(𝑓 Fn 𝑛𝜑𝜓)
45 bnj607.28 . . . . . . . . 9 𝐺 ∈ V
46 nfcv 2948 . . . . . . . . . 10 𝐺
47 nfv 2005 . . . . . . . . . . 11 𝐺 Fn 𝑛
48 bnj607.300 . . . . . . . . . . . 12 (𝜑1[𝐺 / ]𝜑0)
49 nfsbc1v 3653 . . . . . . . . . . . 12 [𝐺 / ]𝜑0
5048, 49nfxfr 1938 . . . . . . . . . . 11 𝜑1
51 bnj607.301 . . . . . . . . . . . 12 (𝜓1[𝐺 / ]𝜓0)
52 nfsbc1v 3653 . . . . . . . . . . . 12 [𝐺 / ]𝜓0
5351, 52nfxfr 1938 . . . . . . . . . . 11 𝜓1
5447, 50, 53nf3an 1993 . . . . . . . . . 10 (𝐺 Fn 𝑛𝜑1𝜓1)
55 fneq1 6186 . . . . . . . . . . 11 ( = 𝐺 → ( Fn 𝑛𝐺 Fn 𝑛))
56 sbceq1a 3644 . . . . . . . . . . . 12 ( = 𝐺 → (𝜑0[𝐺 / ]𝜑0))
5756, 48syl6bbr 280 . . . . . . . . . . 11 ( = 𝐺 → (𝜑0𝜑1))
58 sbceq1a 3644 . . . . . . . . . . . 12 ( = 𝐺 → (𝜓0[𝐺 / ]𝜓0))
5958, 51syl6bbr 280 . . . . . . . . . . 11 ( = 𝐺 → (𝜓0𝜓1))
6055, 57, 593anbi123d 1553 . . . . . . . . . 10 ( = 𝐺 → (( Fn 𝑛𝜑0𝜓0) ↔ (𝐺 Fn 𝑛𝜑1𝜓1)))
6146, 54, 60spcegf 3482 . . . . . . . . 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 31266 . . . . . . . . . . . . 13 (𝜑0 ↔ (‘∅) = pred(𝑥, 𝐴, 𝑅))
6766, 48, 45bnj526 31276 . . . . . . . . . . . 12 (𝜑1 ↔ (𝐺‘∅) = pred(𝑥, 𝐴, 𝑅))
6863, 67bitr4i 269 . . . . . . . . . . 11 (𝜑″𝜑1)
69 bnj607.33 . . . . . . . . . . . 12 (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝐺‘suc 𝑖) = 𝑦 ∈ (𝐺𝑖) pred(𝑦, 𝐴, 𝑅)))
70 bnj607.2 . . . . . . . . . . . . . 14 (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))
71 bnj607.401 . . . . . . . . . . . . . 14 (𝜓0[ / 𝑓]𝜓)
72 vex 3394 . . . . . . . . . . . . . 14 ∈ V
7370, 71, 72bnj540 31280 . . . . . . . . . . . . 13 (𝜓0 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (‘suc 𝑖) = 𝑦 ∈ (𝑖) pred(𝑦, 𝐴, 𝑅)))
7473, 51, 45bnj540 31280 . . . . . . . . . . . 12 (𝜓1 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝐺‘suc 𝑖) = 𝑦 ∈ (𝐺𝑖) pred(𝑦, 𝐴, 𝑅)))
7569, 74bitr4i 269 . . . . . . . . . . 11 (𝜓″𝜓1)
7668, 75anbi12i 614 . . . . . . . . . 10 ((𝜑″𝜓″) ↔ (𝜑1𝜓1))
7776anbi2i 611 . . . . . . . . 9 ((𝐺 Fn 𝑛 ∧ (𝜑″𝜓″)) ↔ (𝐺 Fn 𝑛 ∧ (𝜑1𝜓1)))
78 3anass 1109 . . . . . . . . 9 ((𝐺 Fn 𝑛𝜑″𝜓″) ↔ (𝐺 Fn 𝑛 ∧ (𝜑″𝜓″)))
79 3anass 1109 . . . . . . . . 9 ((𝐺 Fn 𝑛𝜑1𝜓1) ↔ (𝐺 Fn 𝑛 ∧ (𝜑1𝜓1)))
8077, 78, 793bitr4i 294 . . . . . . . 8 ((𝐺 Fn 𝑛𝜑″𝜓″) ↔ (𝐺 Fn 𝑛𝜑1𝜓1))
81 nfv 2005 . . . . . . . . 9 (𝑓 Fn 𝑛𝜑𝜓)
82 nfv 2005 . . . . . . . . . 10 𝑓 Fn 𝑛
83 nfsbc1v 3653 . . . . . . . . . . 11 𝑓[ / 𝑓]𝜑
8464, 83nfxfr 1938 . . . . . . . . . 10 𝑓𝜑0
85 nfsbc1v 3653 . . . . . . . . . . 11 𝑓[ / 𝑓]𝜓
8671, 85nfxfr 1938 . . . . . . . . . 10 𝑓𝜓0
8782, 84, 86nf3an 1993 . . . . . . . . 9 𝑓( Fn 𝑛𝜑0𝜓0)
88 fneq1 6186 . . . . . . . . . 10 (𝑓 = → (𝑓 Fn 𝑛 Fn 𝑛))
89 sbceq1a 3644 . . . . . . . . . . 11 (𝑓 = → (𝜑[ / 𝑓]𝜑))
9089, 64syl6bbr 280 . . . . . . . . . 10 (𝑓 = → (𝜑𝜑0))
91 sbceq1a 3644 . . . . . . . . . . 11 (𝑓 = → (𝜓[ / 𝑓]𝜓))
9291, 71syl6bbr 280 . . . . . . . . . 10 (𝑓 = → (𝜓𝜓0))
9388, 90, 923anbi123d 1553 . . . . . . . . 9 (𝑓 = → ((𝑓 Fn 𝑛𝜑𝜓) ↔ ( Fn 𝑛𝜑0𝜓0)))
9481, 87, 93cbvex 2445 . . . . . . . 8 (∃𝑓(𝑓 Fn 𝑛𝜑𝜓) ↔ ∃( Fn 𝑛𝜑0𝜓0))
9562, 80, 943imtr4i 283 . . . . . . 7 ((𝐺 Fn 𝑛𝜑″𝜓″) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
9644, 95exlimi 2253 . . . . . 6 (∃𝑓(𝐺 Fn 𝑛𝜑″𝜓″) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
9738, 43, 963syl 18 . . . . 5 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ (𝜒′𝜂)) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
9897expcom 400 . . . 4 ((𝜒′𝜂) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
9998exlimivv 2023 . . 3 (∃𝑚𝑝(𝜒′𝜂) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
10011, 24, 993syl 18 . 2 (((𝑛 ≠ 1𝑜𝑛𝐷) ∧ 𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
1011003impa 1129 1 ((𝑛 ≠ 1𝑜𝑛𝐷𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wex 1859  wcel 2156  ∃!weu 2630  wne 2978  wral 3096  Vcvv 3391  [wsbc 3633  c0 4116   ciun 4712   class class class wbr 4844   E cep 5223  suc csuc 5938   Fn wfn 6092  cfv 6097  ωcom 7291  1𝑜c1o 7785  w-bnj17 31073   predc-bnj14 31075   FrSe w-bnj15 31079
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pr 5096
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-eprel 5224  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-fv 6105  df-bnj17 31074
This theorem is referenced by:  bnj600  31307
  Copyright terms: Public domain W3C validator