Theorem bnj849 31813

Description: Technical lemma for bnj69 31896. 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.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)

Hypotheses

Ref	Expression
bnj849.1	⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))
bnj849.2	⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))
bnj849.3	⊢ 𝐷 = (ω ∖ {∅})
bnj849.4	⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}
bnj849.5	⊢ (𝜒 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷))
bnj849.6	⊢ (𝜃 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))
bnj849.7	⊢ (𝜑′ ↔ [𝑔 / 𝑓]𝜑)
bnj849.8	⊢ (𝜓′ ↔ [𝑔 / 𝑓]𝜓)
bnj849.9	⊢ (𝜃′ ↔ [𝑔 / 𝑓]𝜃)
bnj849.10	⊢ (𝜏 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴))

Assertion

Ref	Expression
bnj849	⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ∈ V)

Distinct variable groups:   𝐴,𝑓,𝑖,𝑛,𝑦   𝐵,𝑔   𝐷,𝑓,𝑔,𝑛   𝐷,𝑖   𝑅,𝑓,𝑖,𝑛,𝑦   𝑓,𝑋,𝑛   𝜒,𝑓,𝑔   𝜑,𝑔   𝜓,𝑔   𝜏,𝑔,𝑛   𝜃,𝑔

Allowed substitution hints:   𝜑(𝑦,𝑓,𝑖,𝑛)   𝜓(𝑦,𝑓,𝑖,𝑛)   𝜒(𝑦,𝑖,𝑛)   𝜃(𝑦,𝑓,𝑖,𝑛)   𝜏(𝑦,𝑓,𝑖)   𝐴(𝑔)   𝐵(𝑦,𝑓,𝑖,𝑛)   𝐷(𝑦)   𝑅(𝑔)   𝑋(𝑦,𝑔,𝑖)   𝜑′(𝑦,𝑓,𝑔,𝑖,𝑛)   𝜓′(𝑦,𝑓,𝑔,𝑖,𝑛)   𝜃′(𝑦,𝑓,𝑔,𝑖,𝑛)

Proof of Theorem bnj849

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		bnj849.10	. 2 ⊢ (𝜏 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴))
2		bnj849.1	. . . 4 ⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))
3		bnj849.2	. . . 4 ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))
4		bnj849.3	. . . 4 ⊢ 𝐷 = (ω ∖ {∅})
5		bnj849.5	. . . 4 ⊢ (𝜒 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷))
6		bnj849.6	. . . 4 ⊢ (𝜃 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))
7	2, 3, 4, 5, 6	bnj865 31811	. . 3 ⊢ ∃𝑤∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)
8		bnj849.4	. . . . . . . 8 ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}
9		bnj849.7	. . . . . . . 8 ⊢ (𝜑′ ↔ [𝑔 / 𝑓]𝜑)
10		bnj849.8	. . . . . . . 8 ⊢ (𝜓′ ↔ [𝑔 / 𝑓]𝜓)
11	8, 9, 10	bnj873 31812	. . . . . . 7 ⊢ 𝐵 = {𝑔 ∣ ∃𝑛 ∈ 𝐷 (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)}
12		df-rex 3111	. . . . . . . . 9 ⊢ (∃𝑛 ∈ 𝐷 (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′) ↔ ∃𝑛(𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)))
13		19.29 1855	. . . . . . . . . . 11 ⊢ ((∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ ∃𝑛(𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → ∃𝑛((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))))
14		an12 641	. . . . . . . . . . . . 13 ⊢ (((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) ↔ (𝑛 ∈ 𝐷 ∧ ((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))))
15		df-3an 1082	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑛 ∈ 𝐷))
16	1	anbi1i 623	. . . . . . . . . . . . . . . 16 ⊢ ((𝜏 ∧ 𝑛 ∈ 𝐷) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑛 ∈ 𝐷))
17	15, 5, 16	3bitr4i 304	. . . . . . . . . . . . . . 15 ⊢ (𝜒 ↔ (𝜏 ∧ 𝑛 ∈ 𝐷))
18		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝜒)
19		bnj849.9	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜃′ ↔ [𝑔 / 𝑓]𝜃)
20	6, 9, 10, 19	bnj581 31796	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜃′ ↔ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))
21	19, 20	bitr3i 278	. . . . . . . . . . . . . . . . . . 19 ⊢ ([𝑔 / 𝑓]𝜃 ↔ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))
22	2, 3, 4, 5, 6	bnj864 31810	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → ∃!𝑓𝜃)
23		df-rex 3111	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑓 ∈ 𝑤 𝜃 ↔ ∃𝑓(𝑓 ∈ 𝑤 ∧ 𝜃))
24		exancom 1842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑓(𝑓 ∈ 𝑤 ∧ 𝜃) ↔ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤))
25	23, 24	sylbb 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑓 ∈ 𝑤 𝜃 → ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤))
26		nfeu1 2635	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑓∃!𝑓𝜃
27		nfe1 2120	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑓∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)
28	26, 27	nfan 1881	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑓(∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤))
29		nfsbc1v 3726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑓[𝑔 / 𝑓]𝜃
30		nfv 1892	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑓 𝑔 ∈ 𝑤
31	29, 30	nfim 1878	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑓([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤)
32	28, 31	nfim 1878	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑓((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤))
33		sbceq1a 3717	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → (𝜃 ↔ [𝑔 / 𝑓]𝜃))
34		elequ1 2088	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → (𝑓 ∈ 𝑤 ↔ 𝑔 ∈ 𝑤))
35	33, 34	imbi12d 346	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝑔 → ((𝜃 → 𝑓 ∈ 𝑤) ↔ ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤)))
36	35	imbi2d 342	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝑔 → (((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → (𝜃 → 𝑓 ∈ 𝑤)) ↔ ((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤))))
37		eupick 2688	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → (𝜃 → 𝑓 ∈ 𝑤))
38	32, 36, 37	chvar 2369	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤))
39	22, 25, 38	syl2an 595	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ ∃𝑓 ∈ 𝑤 𝜃) → ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤))
40	21, 39	syl5bir 244	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ ∃𝑓 ∈ 𝑤 𝜃) → ((𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′) → 𝑔 ∈ 𝑤))
41	40	ex 413	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (∃𝑓 ∈ 𝑤 𝜃 → ((𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′) → 𝑔 ∈ 𝑤)))
42	18, 41	embantd 59	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → ((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) → ((𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′) → 𝑔 ∈ 𝑤)))
43	42	impd 411	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)) → 𝑔 ∈ 𝑤))
44	17, 43	sylbir 236	. . . . . . . . . . . . . 14 ⊢ ((𝜏 ∧ 𝑛 ∈ 𝐷) → (((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)) → 𝑔 ∈ 𝑤))
45	44	expimpd 454	. . . . . . . . . . . . 13 ⊢ (𝜏 → ((𝑛 ∈ 𝐷 ∧ ((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → 𝑔 ∈ 𝑤))
46	14, 45	syl5bi 243	. . . . . . . . . . . 12 ⊢ (𝜏 → (((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → 𝑔 ∈ 𝑤))
47	46	exlimdv 1911	. . . . . . . . . . 11 ⊢ (𝜏 → (∃𝑛((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → 𝑔 ∈ 𝑤))
48	13, 47	syl5 34	. . . . . . . . . 10 ⊢ (𝜏 → ((∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ ∃𝑛(𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → 𝑔 ∈ 𝑤))
49	48	expdimp 453	. . . . . . . . 9 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → (∃𝑛(𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)) → 𝑔 ∈ 𝑤))
50	12, 49	syl5bi 243	. . . . . . . 8 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → (∃𝑛 ∈ 𝐷 (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′) → 𝑔 ∈ 𝑤))
51	50	abssdv 3966	. . . . . . 7 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → {𝑔 ∣ ∃𝑛 ∈ 𝐷 (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)} ⊆ 𝑤)
52	11, 51	syl5eqss 3936	. . . . . 6 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → 𝐵 ⊆ 𝑤)
53		vex 3440	. . . . . . 7 ⊢ 𝑤 ∈ V
54	53	ssex 5116	. . . . . 6 ⊢ (𝐵 ⊆ 𝑤 → 𝐵 ∈ V)
55	52, 54	syl 17	. . . . 5 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → 𝐵 ∈ V)
56	55	ex 413	. . . 4 ⊢ (𝜏 → (∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) → 𝐵 ∈ V))
57	56	exlimdv 1911	. . 3 ⊢ (𝜏 → (∃𝑤∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) → 𝐵 ∈ V))
58	7, 57	mpi 20	. 2 ⊢ (𝜏 → 𝐵 ∈ V)
59	1, 58	sylbir 236	1 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ∈ V)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1080  ∀wal 1520   = wceq 1522  ∃wex 1761   ∈ wcel 2081  ∃!weu 2611  {cab 2775  ∀wral 3105  ∃wrex 3106  Vcvv 3437  [wsbc 3706   ∖ cdif 3856   ⊆ wss 3859  ∅c0 4211  {csn 4472  ∪ ciun 4825  suc csuc 6068   Fn wfn 6220  ‘cfv 6225  ωcom 7436   predc-bnj14 31575   FrSe w-bnj15 31579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-reg 8902  ax-inf2 8950

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-fal 1535  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-reu 3112  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-iun 4827  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-om 7437  df-1o 7953  df-bnj17 31574  df-bnj14 31576  df-bnj13 31578  df-bnj15 31580

This theorem is referenced by:  bnj893  31816