Theorem bnj908 34967

Description: Technical lemma for bnj69 35046. 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
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

Ref	Expression
bnj908	⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂) → ∃𝑓(𝐺 Fn 𝑛 ∧ 𝜑″ ∧ 𝜓″))

Distinct variable groups:   𝐴,𝑓,𝑖,𝑚,𝑛,𝑝   𝑦,𝐴,𝑓,𝑖,𝑛,𝑝   𝐷,𝑝   𝑖,𝐺,𝑦   𝑅,𝑓,𝑖,𝑚,𝑛,𝑝   𝑦,𝑅   𝜂,𝑓,𝑖   𝑥,𝑓,𝑚,𝑛,𝑝   𝑖,𝜑′,𝑝   𝜑,𝑚,𝑝   𝜓,𝑚,𝑝   𝜃,𝑝

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑓,𝑖,𝑛)   𝜓(𝑥,𝑦,𝑓,𝑖,𝑛)   𝜒(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝜃(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛)   𝜏(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝜂(𝑥,𝑦,𝑚,𝑛,𝑝)   𝜁(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝜎(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝜌(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝐴(𝑥)   𝐵(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝐶(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝐷(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛)   𝑅(𝑥)   𝐺(𝑥,𝑓,𝑚,𝑛,𝑝)   𝐾(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝐿(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝜑′(𝑥,𝑦,𝑓,𝑚,𝑛)   𝜓′(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝜒′(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝜑″(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝜓″(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝜒″(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)

Proof of Theorem bnj908

Step	Hyp	Ref	Expression
1		bnj248 34736	. . . . . 6 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂) ↔ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜒′) ∧ 𝜂))
2		bnj908.4	. . . . . . . . . . 11 ⊢ (𝜒 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))
3		bnj908.10	. . . . . . . . . . 11 ⊢ (𝜑′ ↔ [𝑚 / 𝑛]𝜑)
4		bnj908.11	. . . . . . . . . . 11 ⊢ (𝜓′ ↔ [𝑚 / 𝑛]𝜓)
5		bnj908.12	. . . . . . . . . . 11 ⊢ (𝜒′ ↔ [𝑚 / 𝑛]𝜒)
6		vex 3468	. . . . . . . . . . 11 ⊢ 𝑚 ∈ V
7	2, 3, 4, 5, 6	bnj207 34917	. . . . . . . . . 10 ⊢ (𝜒′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)))
8	7	biimpi 216	. . . . . . . . 9 ⊢ (𝜒′ → ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)))
9		euex 2577	. . . . . . . . 9 ⊢ (∃!𝑓(𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′) → ∃𝑓(𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))
10	8, 9	syl6 35	. . . . . . . 8 ⊢ (𝜒′ → ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑓(𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)))
11	10	impcom 407	. . . . . . 7 ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜒′) → ∃𝑓(𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))
12		bnj908.17	. . . . . . 7 ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))
13	11, 12	bnj1198 34831	. . . . . 6 ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜒′) → ∃𝑓𝜏)
14	1, 13	bnj832 34794	. . . . 5 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂) → ∃𝑓𝜏)
15		bnj645 34786	. . . . 5 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂) → 𝜂)
16		19.41v 1949	. . . . 5 ⊢ (∃𝑓(𝜏 ∧ 𝜂) ↔ (∃𝑓𝜏 ∧ 𝜂))
17	14, 15, 16	sylanbrc 583	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂) → ∃𝑓(𝜏 ∧ 𝜂))
18		bnj642 34784	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂) → 𝑅 FrSe 𝐴)
19		19.41v 1949	. . . 4 ⊢ (∃𝑓((𝜏 ∧ 𝜂) ∧ 𝑅 FrSe 𝐴) ↔ (∃𝑓(𝜏 ∧ 𝜂) ∧ 𝑅 FrSe 𝐴))
20	17, 18, 19	sylanbrc 583	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂) → ∃𝑓((𝜏 ∧ 𝜂) ∧ 𝑅 FrSe 𝐴))
21		bnj170 34734	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) ↔ ((𝜏 ∧ 𝜂) ∧ 𝑅 FrSe 𝐴))
22	20, 21	bnj1198 34831	. 2 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂) → ∃𝑓(𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂))
23		bnj908.18	. . . 4 ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))
24		bnj908.19	. . . 4 ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))
25		bnj908.1	. . . . . 6 ⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
26	25, 3, 6	bnj523 34923	. . . . 5 ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
27		bnj908.2	. . . . . 6 ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))
28	27, 4, 6	bnj539 34927	. . . . 5 ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))
29		bnj908.3	. . . . 5 ⊢ 𝐷 = (ω ∖ {∅})
30		bnj908.16	. . . . 5 ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩})
31	26, 28, 29, 30, 12, 23	bnj544 34930	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛)
32	23, 24, 31	bnj561 34939	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝐺 Fn 𝑛)
33		bnj908.13	. . . . . 6 ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑)
34	30	bnj528 34925	. . . . . 6 ⊢ 𝐺 ∈ V
35	25, 33, 34	bnj609 34953	. . . . 5 ⊢ (𝜑″ ↔ (𝐺‘∅) = pred(𝑥, 𝐴, 𝑅))
36	26, 29, 30, 12, 23, 31, 35	bnj545 34931	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝜑″)
37	23, 24, 36	bnj562 34940	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝜑″)
38		bnj908.20	. . . 4 ⊢ (𝜁 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖))
39		bnj908.22	. . . 4 ⊢ 𝐵 = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)
40		bnj908.23	. . . 4 ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)
41		bnj908.24	. . . 4 ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)
42		bnj908.25	. . . 4 ⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅)
43		bnj908.26	. . . 4 ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, 𝐶⟩})
44		bnj908.21	. . . 4 ⊢ (𝜌 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖))
45		bnj908.14	. . . . 5 ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓)
46	27, 45, 34	bnj611 34954	. . . 4 ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)))
47	29, 30, 12, 23, 24, 38, 39, 40, 41, 42, 43, 26, 28, 31, 44, 32, 46	bnj571 34942	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝜓″)
48	32, 37, 47	3jca 1128	. 2 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → (𝐺 Fn 𝑛 ∧ 𝜑″ ∧ 𝜓″))
49	22, 48	bnj593 34781	1 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂) → ∃𝑓(𝐺 Fn 𝑛 ∧ 𝜑″ ∧ 𝜓″))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∃!weu 2568   ≠ wne 2933  ∀wral 3052  [wsbc 3770   ∖ cdif 3928   ∪ cun 3929  ∅c0 4313  {csn 4606  ⟨cop 4612  ∪ ciun 4972   class class class wbr 5124   E cep 5557  suc csuc 6359   Fn wfn 6531  ‘cfv 6536  ωcom 7866   ∧ w-bnj17 34722   predc-bnj14 34724   FrSe w-bnj15 34728

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-rep 5254  ax-sep 5271  ax-nul 5281  ax-pr 5407  ax-un 7734  ax-reg 9611

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-sbc 3771  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-iun 4974  df-br 5125  df-opab 5187  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-res 5671  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-fv 6544  df-om 7867  df-bnj17 34723  df-bnj14 34725  df-bnj13 34727  df-bnj15 34729

This theorem is referenced by: (None)