Theorem bnj849 35283

Description: Technical lemma for bnj69 35368. 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 35281	. . 3 ⊢ ∃𝑤∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)
8		bnj849.4	. . . . . . . 8 ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}
9		bnj849.7	. . . . . . . 8 ⊢ (𝜑′ ↔ [𝑔 / 𝑓]𝜑)
10		bnj849.8	. . . . . . . 8 ⊢ (𝜓′ ↔ [𝑔 / 𝑓]𝜓)
11	8, 9, 10	bnj873 35282	. . . . . . 7 ⊢ 𝐵 = {𝑔 ∣ ∃𝑛 ∈ 𝐷 (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)}
12		df-rex 3097	. . . . . . . . 9 ⊢ (∃𝑛 ∈ 𝐷 (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′) ↔ ∃𝑛(𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)))
13		19.29 1901	. . . . . . . . . . 11 ⊢ ((∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ ∃𝑛(𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → ∃𝑛((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))))
14		an12 657	. . . . . . . . . . . . 13 ⊢ (((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) ↔ (𝑛 ∈ 𝐷 ∧ ((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))))
15		df-3an 1103	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑛 ∈ 𝐷))
16	1	anbi1i 635	. . . . . . . . . . . . . . . 16 ⊢ ((𝜏 ∧ 𝑛 ∈ 𝐷) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑛 ∈ 𝐷))
17	15, 5, 16	3bitr4i 306	. . . . . . . . . . . . . . 15 ⊢ (𝜒 ↔ (𝜏 ∧ 𝑛 ∈ 𝐷))
18		id 23	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝜒)
19		bnj849.9	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜃′ ↔ [𝑔 / 𝑓]𝜃)
20	6, 9, 10, 19	bnj581 35266	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜃′ ↔ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))
21	19, 20	bitr3i 280	. . . . . . . . . . . . . . . . . . 19 ⊢ ([𝑔 / 𝑓]𝜃 ↔ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))
22	2, 3, 4, 5, 6	bnj864 35280	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → ∃!𝑓𝜃)
23		df-rex 3097	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑓 ∈ 𝑤 𝜃 ↔ ∃𝑓(𝑓 ∈ 𝑤 ∧ 𝜃))
24		exancom 1889	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑓(𝑓 ∈ 𝑤 ∧ 𝜃) ↔ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤))
25	23, 24	sylbb 222	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑓 ∈ 𝑤 𝜃 → ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤))
26		nfeu1 2624	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑓∃!𝑓𝜃
27		nfe1 2192	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑓∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)
28	26, 27	nfan 1927	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑓(∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤))
29		nfsbc1v 3772	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑓[𝑔 / 𝑓]𝜃
30		nfv 1942	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑓 𝑔 ∈ 𝑤
31	29, 30	nfim 1924	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑓([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤)
32	28, 31	nfim 1924	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑓((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤))
33		sbceq1a 3763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → (𝜃 ↔ [𝑔 / 𝑓]𝜃))
34		elequ1 2157	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → (𝑓 ∈ 𝑤 ↔ 𝑔 ∈ 𝑤))
35	33, 34	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝑔 → ((𝜃 → 𝑓 ∈ 𝑤) ↔ ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤)))
36	35	imbi2d 343	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝑔 → (((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → (𝜃 → 𝑓 ∈ 𝑤)) ↔ ((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤))))
37		eupick 2668	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → (𝜃 → 𝑓 ∈ 𝑤))
38	32, 36, 37	chvarfv 2283	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤))
39	22, 25, 38	syl2an 607	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ ∃𝑓 ∈ 𝑤 𝜃) → ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤))
40	21, 39	biimtrrid 246	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ ∃𝑓 ∈ 𝑤 𝜃) → ((𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′) → 𝑔 ∈ 𝑤))
41	40	ex 417	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (∃𝑓 ∈ 𝑤 𝜃 → ((𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′) → 𝑔 ∈ 𝑤)))
42	18, 41	embantd 60	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → ((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) → ((𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′) → 𝑔 ∈ 𝑤)))
43	42	impd 415	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)) → 𝑔 ∈ 𝑤))
44	17, 43	sylbir 238	. . . . . . . . . . . . . 14 ⊢ ((𝜏 ∧ 𝑛 ∈ 𝐷) → (((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)) → 𝑔 ∈ 𝑤))
45	44	expimpd 458	. . . . . . . . . . . . 13 ⊢ (𝜏 → ((𝑛 ∈ 𝐷 ∧ ((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → 𝑔 ∈ 𝑤))
46	14, 45	biimtrid 245	. . . . . . . . . . . 12 ⊢ (𝜏 → (((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → 𝑔 ∈ 𝑤))
47	46	exlimdv 1961	. . . . . . . . . . 11 ⊢ (𝜏 → (∃𝑛((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → 𝑔 ∈ 𝑤))
48	13, 47	syl5 35	. . . . . . . . . 10 ⊢ (𝜏 → ((∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ ∃𝑛(𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → 𝑔 ∈ 𝑤))
49	48	expdimp 457	. . . . . . . . 9 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → (∃𝑛(𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)) → 𝑔 ∈ 𝑤))
50	12, 49	biimtrid 245	. . . . . . . 8 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → (∃𝑛 ∈ 𝐷 (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′) → 𝑔 ∈ 𝑤))
51	50	abssdv 4029	. . . . . . 7 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → {𝑔 ∣ ∃𝑛 ∈ 𝐷 (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)} ⊆ 𝑤)
52	11, 51	eqsstrid 3983	. . . . . 6 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → 𝐵 ⊆ 𝑤)
53		vex 3466	. . . . . . 7 ⊢ 𝑤 ∈ V
54	53	ssex 5295	. . . . . 6 ⊢ (𝐵 ⊆ 𝑤 → 𝐵 ∈ V)
55	52, 54	syl 18	. . . . 5 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → 𝐵 ∈ V)
56	55	ex 417	. . . 4 ⊢ (𝜏 → (∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) → 𝐵 ∈ V))
57	56	exlimdv 1961	. . 3 ⊢ (𝜏 → (∃𝑤∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) → 𝐵 ∈ V))
58	7, 57	mpi 21	. 2 ⊢ (𝜏 → 𝐵 ∈ V)
59	1, 58	sylbir 238	1 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ∈ V)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101  ∀wal 1566   = wceq 1568  ∃wex 1807   ∈ wcel 2150  ∃!weu 2603  {cab 2748  ∀wral 3086  ∃wrex 3096  Vcvv 3462  [wsbc 3752   ∖ cdif 3910   ⊆ wss 3913  ∅c0 4294  {csn 4594  ∪ ciun 4961  suc csuc 6366   Fn wfn 6535  ‘cfv 6540  ωcom 7865   predc-bnj14 35047   FrSe w-bnj15 35051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-10 2183  ax-11 2199  ax-12 2220  ax-ext 2742  ax-rep 5243  ax-sep 5262  ax-nul 5274  ax-pow 5340  ax-pr 5408  ax-un 7736  ax-reg 9557  ax-inf2 9613

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2099  df-mo 2574  df-eu 2604  df-clab 2749  df-cleq 2762  df-clel 2845  df-nfc 2919  df-ne 2966  df-ral 3087  df-rex 3097  df-reu 3377  df-rab 3424  df-v 3464  df-sbc 3753  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5560  df-eprel 5565  df-po 5573  df-so 5574  df-fr 5618  df-we 5620  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-om 7866  df-1o 8456  df-bnj17 35046  df-bnj14 35048  df-bnj13 35050  df-bnj15 35052

This theorem is referenced by:  bnj893  35286