Theorem bnj849 33931

Description: Technical lemma for bnj69 34016. 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 33929	. . 3 ⊢ ∃𝑤∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)
8		bnj849.4	. . . . . . . 8 ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}
9		bnj849.7	. . . . . . . 8 ⊢ (𝜑′ ↔ [𝑔 / 𝑓]𝜑)
10		bnj849.8	. . . . . . . 8 ⊢ (𝜓′ ↔ [𝑔 / 𝑓]𝜓)
11	8, 9, 10	bnj873 33930	. . . . . . 7 ⊢ 𝐵 = {𝑔 ∣ ∃𝑛 ∈ 𝐷 (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)}
12		df-rex 3071	. . . . . . . . 9 ⊢ (∃𝑛 ∈ 𝐷 (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′) ↔ ∃𝑛(𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)))
13		19.29 1876	. . . . . . . . . . 11 ⊢ ((∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ ∃𝑛(𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → ∃𝑛((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))))
14		an12 643	. . . . . . . . . . . . 13 ⊢ (((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) ↔ (𝑛 ∈ 𝐷 ∧ ((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))))
15		df-3an 1089	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑛 ∈ 𝐷))
16	1	anbi1i 624	. . . . . . . . . . . . . . . 16 ⊢ ((𝜏 ∧ 𝑛 ∈ 𝐷) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑛 ∈ 𝐷))
17	15, 5, 16	3bitr4i 302	. . . . . . . . . . . . . . 15 ⊢ (𝜒 ↔ (𝜏 ∧ 𝑛 ∈ 𝐷))
18		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝜒)
19		bnj849.9	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜃′ ↔ [𝑔 / 𝑓]𝜃)
20	6, 9, 10, 19	bnj581 33914	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜃′ ↔ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))
21	19, 20	bitr3i 276	. . . . . . . . . . . . . . . . . . 19 ⊢ ([𝑔 / 𝑓]𝜃 ↔ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))
22	2, 3, 4, 5, 6	bnj864 33928	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → ∃!𝑓𝜃)
23		df-rex 3071	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑓 ∈ 𝑤 𝜃 ↔ ∃𝑓(𝑓 ∈ 𝑤 ∧ 𝜃))
24		exancom 1864	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑓(𝑓 ∈ 𝑤 ∧ 𝜃) ↔ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤))
25	23, 24	sylbb 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑓 ∈ 𝑤 𝜃 → ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤))
26		nfeu1 2582	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑓∃!𝑓𝜃
27		nfe1 2147	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑓∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)
28	26, 27	nfan 1902	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑓(∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤))
29		nfsbc1v 3797	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑓[𝑔 / 𝑓]𝜃
30		nfv 1917	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑓 𝑔 ∈ 𝑤
31	29, 30	nfim 1899	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑓([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤)
32	28, 31	nfim 1899	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑓((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤))
33		sbceq1a 3788	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → (𝜃 ↔ [𝑔 / 𝑓]𝜃))
34		elequ1 2113	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → (𝑓 ∈ 𝑤 ↔ 𝑔 ∈ 𝑤))
35	33, 34	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝑔 → ((𝜃 → 𝑓 ∈ 𝑤) ↔ ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤)))
36	35	imbi2d 340	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝑔 → (((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → (𝜃 → 𝑓 ∈ 𝑤)) ↔ ((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤))))
37		eupick 2629	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → (𝜃 → 𝑓 ∈ 𝑤))
38	32, 36, 37	chvarfv 2233	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤))
39	22, 25, 38	syl2an 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ ∃𝑓 ∈ 𝑤 𝜃) → ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤))
40	21, 39	biimtrrid 242	. . . . . . . . . . . . . . . . . 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 234	. . . . . . . . . . . . . 14 ⊢ ((𝜏 ∧ 𝑛 ∈ 𝐷) → (((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)) → 𝑔 ∈ 𝑤))
45	44	expimpd 454	. . . . . . . . . . . . 13 ⊢ (𝜏 → ((𝑛 ∈ 𝐷 ∧ ((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → 𝑔 ∈ 𝑤))
46	14, 45	biimtrid 241	. . . . . . . . . . . 12 ⊢ (𝜏 → (((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → 𝑔 ∈ 𝑤))
47	46	exlimdv 1936	. . . . . . . . . . 11 ⊢ (𝜏 → (∃𝑛((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → 𝑔 ∈ 𝑤))
48	13, 47	syl5 34	. . . . . . . . . 10 ⊢ (𝜏 → ((∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ ∃𝑛(𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → 𝑔 ∈ 𝑤))
49	48	expdimp 453	. . . . . . . . 9 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → (∃𝑛(𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)) → 𝑔 ∈ 𝑤))
50	12, 49	biimtrid 241	. . . . . . . 8 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → (∃𝑛 ∈ 𝐷 (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′) → 𝑔 ∈ 𝑤))
51	50	abssdv 4065	. . . . . . 7 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → {𝑔 ∣ ∃𝑛 ∈ 𝐷 (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)} ⊆ 𝑤)
52	11, 51	eqsstrid 4030	. . . . . 6 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → 𝐵 ⊆ 𝑤)
53		vex 3478	. . . . . . 7 ⊢ 𝑤 ∈ V
54	53	ssex 5321	. . . . . 6 ⊢ (𝐵 ⊆ 𝑤 → 𝐵 ∈ V)
55	52, 54	syl 17	. . . . 5 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → 𝐵 ∈ V)
56	55	ex 413	. . . 4 ⊢ (𝜏 → (∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) → 𝐵 ∈ V))
57	56	exlimdv 1936	. . 3 ⊢ (𝜏 → (∃𝑤∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) → 𝐵 ∈ V))
58	7, 57	mpi 20	. 2 ⊢ (𝜏 → 𝐵 ∈ V)
59	1, 58	sylbir 234	1 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ∈ V)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087  ∀wal 1539   = wceq 1541  ∃wex 1781   ∈ wcel 2106  ∃!weu 2562  {cab 2709  ∀wral 3061  ∃wrex 3070  Vcvv 3474  [wsbc 3777   ∖ cdif 3945   ⊆ wss 3948  ∅c0 4322  {csn 4628  ∪ ciun 4997  suc csuc 6366   Fn wfn 6538  ‘cfv 6543  ωcom 7854   predc-bnj14 33694   FrSe w-bnj15 33698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-reg 9586  ax-inf2 9635

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-om 7855  df-1o 8465  df-bnj17 33693  df-bnj14 33695  df-bnj13 33697  df-bnj15 33699

This theorem is referenced by:  bnj893  33934