Theorem bnj849 35122

Description: Technical lemma for bnj69 35207. 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 35120	. . 3 ⊢ ∃𝑤∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)
8		bnj849.4	. . . . . . . 8 ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}
9		bnj849.7	. . . . . . . 8 ⊢ (𝜑′ ↔ [𝑔 / 𝑓]𝜑)
10		bnj849.8	. . . . . . . 8 ⊢ (𝜓′ ↔ [𝑔 / 𝑓]𝜓)
11	8, 9, 10	bnj873 35121	. . . . . . 7 ⊢ 𝐵 = {𝑔 ∣ ∃𝑛 ∈ 𝐷 (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)}
12		df-rex 3066	. . . . . . . . 9 ⊢ (∃𝑛 ∈ 𝐷 (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′) ↔ ∃𝑛(𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)))
13		19.29 1881	. . . . . . . . . . 11 ⊢ ((∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ ∃𝑛(𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → ∃𝑛((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))))
14		an12 652	. . . . . . . . . . . . 13 ⊢ (((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) ↔ (𝑛 ∈ 𝐷 ∧ ((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))))
15		df-3an 1095	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑛 ∈ 𝐷))
16	1	anbi1i 631	. . . . . . . . . . . . . . . 16 ⊢ ((𝜏 ∧ 𝑛 ∈ 𝐷) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑛 ∈ 𝐷))
17	15, 5, 16	3bitr4i 305	. . . . . . . . . . . . . . 15 ⊢ (𝜒 ↔ (𝜏 ∧ 𝑛 ∈ 𝐷))
18		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝜒)
19		bnj849.9	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜃′ ↔ [𝑔 / 𝑓]𝜃)
20	6, 9, 10, 19	bnj581 35105	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜃′ ↔ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))
21	19, 20	bitr3i 279	. . . . . . . . . . . . . . . . . . 19 ⊢ ([𝑔 / 𝑓]𝜃 ↔ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))
22	2, 3, 4, 5, 6	bnj864 35119	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → ∃!𝑓𝜃)
23		df-rex 3066	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑓 ∈ 𝑤 𝜃 ↔ ∃𝑓(𝑓 ∈ 𝑤 ∧ 𝜃))
24		exancom 1869	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑓(𝑓 ∈ 𝑤 ∧ 𝜃) ↔ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤))
25	23, 24	sylbb 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑓 ∈ 𝑤 𝜃 → ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤))
26		nfeu1 2595	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑓∃!𝑓𝜃
27		nfe1 2163	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑓∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)
28	26, 27	nfan 1907	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑓(∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤))
29		nfsbc1v 3745	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑓[𝑔 / 𝑓]𝜃
30		nfv 1922	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑓 𝑔 ∈ 𝑤
31	29, 30	nfim 1904	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑓([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤)
32	28, 31	nfim 1904	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑓((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤))
33		sbceq1a 3736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → (𝜃 ↔ [𝑔 / 𝑓]𝜃))
34		elequ1 2128	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → (𝑓 ∈ 𝑤 ↔ 𝑔 ∈ 𝑤))
35	33, 34	imbi12d 346	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝑔 → ((𝜃 → 𝑓 ∈ 𝑤) ↔ ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤)))
36	35	imbi2d 342	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝑔 → (((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → (𝜃 → 𝑓 ∈ 𝑤)) ↔ ((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤))))
37		eupick 2639	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → (𝜃 → 𝑓 ∈ 𝑤))
38	32, 36, 37	chvarfv 2254	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤))
39	22, 25, 38	syl2an 603	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ ∃𝑓 ∈ 𝑤 𝜃) → ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤))
40	21, 39	biimtrrid 245	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ ∃𝑓 ∈ 𝑤 𝜃) → ((𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′) → 𝑔 ∈ 𝑤))
41	40	ex 414	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (∃𝑓 ∈ 𝑤 𝜃 → ((𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′) → 𝑔 ∈ 𝑤)))
42	18, 41	embantd 59	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → ((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) → ((𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′) → 𝑔 ∈ 𝑤)))
43	42	impd 412	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)) → 𝑔 ∈ 𝑤))
44	17, 43	sylbir 237	. . . . . . . . . . . . . 14 ⊢ ((𝜏 ∧ 𝑛 ∈ 𝐷) → (((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)) → 𝑔 ∈ 𝑤))
45	44	expimpd 455	. . . . . . . . . . . . 13 ⊢ (𝜏 → ((𝑛 ∈ 𝐷 ∧ ((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → 𝑔 ∈ 𝑤))
46	14, 45	biimtrid 244	. . . . . . . . . . . 12 ⊢ (𝜏 → (((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → 𝑔 ∈ 𝑤))
47	46	exlimdv 1941	. . . . . . . . . . 11 ⊢ (𝜏 → (∃𝑛((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → 𝑔 ∈ 𝑤))
48	13, 47	syl5 34	. . . . . . . . . 10 ⊢ (𝜏 → ((∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ ∃𝑛(𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → 𝑔 ∈ 𝑤))
49	48	expdimp 454	. . . . . . . . 9 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → (∃𝑛(𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)) → 𝑔 ∈ 𝑤))
50	12, 49	biimtrid 244	. . . . . . . 8 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → (∃𝑛 ∈ 𝐷 (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′) → 𝑔 ∈ 𝑤))
51	50	abssdv 4001	. . . . . . 7 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → {𝑔 ∣ ∃𝑛 ∈ 𝐷 (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)} ⊆ 𝑤)
52	11, 51	eqsstrid 3955	. . . . . 6 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → 𝐵 ⊆ 𝑤)
53		vex 3437	. . . . . . 7 ⊢ 𝑤 ∈ V
54	53	ssex 5252	. . . . . 6 ⊢ (𝐵 ⊆ 𝑤 → 𝐵 ∈ V)
55	52, 54	syl 17	. . . . 5 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → 𝐵 ∈ V)
56	55	ex 414	. . . 4 ⊢ (𝜏 → (∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) → 𝐵 ∈ V))
57	56	exlimdv 1941	. . 3 ⊢ (𝜏 → (∃𝑤∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) → 𝐵 ∈ V))
58	7, 57	mpi 20	. 2 ⊢ (𝜏 → 𝐵 ∈ V)
59	1, 58	sylbir 237	1 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ∈ V)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   ∧ w3a 1093  ∀wal 1546   = wceq 1548  ∃wex 1787   ∈ wcel 2121  ∃!weu 2574  {cab 2719  ∀wral 3055  ∃wrex 3065  Vcvv 3433  [wsbc 3725   ∖ cdif 3882   ⊆ wss 3885  ∅c0 4264  {csn 4558  ∪ ciun 4924  suc csuc 6316   Fn wfn 6484  ‘cfv 6489  ωcom 7810   predc-bnj14 34886   FrSe w-bnj15 34890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-rep 5202  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682  ax-reg 9501  ax-inf2 9557

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-iun 4926  df-br 5076  df-opab 5138  df-mpt 5157  df-tr 5183  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-om 7811  df-1o 8399  df-bnj17 34885  df-bnj14 34887  df-bnj13 34889  df-bnj15 34891

This theorem is referenced by:  bnj893  35125