Theorem bnj849 34940

Description: Technical lemma for bnj69 35025. 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 34938	. . 3 ⊢ ∃𝑤∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)
8		bnj849.4	. . . . . . . 8 ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}
9		bnj849.7	. . . . . . . 8 ⊢ (𝜑′ ↔ [𝑔 / 𝑓]𝜑)
10		bnj849.8	. . . . . . . 8 ⊢ (𝜓′ ↔ [𝑔 / 𝑓]𝜓)
11	8, 9, 10	bnj873 34939	. . . . . . 7 ⊢ 𝐵 = {𝑔 ∣ ∃𝑛 ∈ 𝐷 (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)}
12		df-rex 3070	. . . . . . . . 9 ⊢ (∃𝑛 ∈ 𝐷 (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′) ↔ ∃𝑛(𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)))
13		19.29 1872	. . . . . . . . . . 11 ⊢ ((∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ ∃𝑛(𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → ∃𝑛((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))))
14		an12 645	. . . . . . . . . . . . 13 ⊢ (((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) ↔ (𝑛 ∈ 𝐷 ∧ ((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))))
15		df-3an 1088	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑛 ∈ 𝐷))
16	1	anbi1i 624	. . . . . . . . . . . . . . . 16 ⊢ ((𝜏 ∧ 𝑛 ∈ 𝐷) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑛 ∈ 𝐷))
17	15, 5, 16	3bitr4i 303	. . . . . . . . . . . . . . 15 ⊢ (𝜒 ↔ (𝜏 ∧ 𝑛 ∈ 𝐷))
18		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝜒)
19		bnj849.9	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜃′ ↔ [𝑔 / 𝑓]𝜃)
20	6, 9, 10, 19	bnj581 34923	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜃′ ↔ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))
21	19, 20	bitr3i 277	. . . . . . . . . . . . . . . . . . 19 ⊢ ([𝑔 / 𝑓]𝜃 ↔ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))
22	2, 3, 4, 5, 6	bnj864 34937	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → ∃!𝑓𝜃)
23		df-rex 3070	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑓 ∈ 𝑤 𝜃 ↔ ∃𝑓(𝑓 ∈ 𝑤 ∧ 𝜃))
24		exancom 1860	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑓(𝑓 ∈ 𝑤 ∧ 𝜃) ↔ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤))
25	23, 24	sylbb 219	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑓 ∈ 𝑤 𝜃 → ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤))
26		nfeu1 2587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑓∃!𝑓𝜃
27		nfe1 2149	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑓∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)
28	26, 27	nfan 1898	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑓(∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤))
29		nfsbc1v 3807	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑓[𝑔 / 𝑓]𝜃
30		nfv 1913	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑓 𝑔 ∈ 𝑤
31	29, 30	nfim 1895	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑓([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤)
32	28, 31	nfim 1895	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑓((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤))
33		sbceq1a 3798	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → (𝜃 ↔ [𝑔 / 𝑓]𝜃))
34		elequ1 2114	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → (𝑓 ∈ 𝑤 ↔ 𝑔 ∈ 𝑤))
35	33, 34	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝑔 → ((𝜃 → 𝑓 ∈ 𝑤) ↔ ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤)))
36	35	imbi2d 340	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝑔 → (((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → (𝜃 → 𝑓 ∈ 𝑤)) ↔ ((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤))))
37		eupick 2632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → (𝜃 → 𝑓 ∈ 𝑤))
38	32, 36, 37	chvarfv 2239	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∃!𝑓𝜃 ∧ ∃𝑓(𝜃 ∧ 𝑓 ∈ 𝑤)) → ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤))
39	22, 25, 38	syl2an 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ ∃𝑓 ∈ 𝑤 𝜃) → ([𝑔 / 𝑓]𝜃 → 𝑔 ∈ 𝑤))
40	21, 39	biimtrrid 243	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ ∃𝑓 ∈ 𝑤 𝜃) → ((𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′) → 𝑔 ∈ 𝑤))
41	40	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (∃𝑓 ∈ 𝑤 𝜃 → ((𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′) → 𝑔 ∈ 𝑤)))
42	18, 41	embantd 59	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → ((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) → ((𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′) → 𝑔 ∈ 𝑤)))
43	42	impd 410	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)) → 𝑔 ∈ 𝑤))
44	17, 43	sylbir 235	. . . . . . . . . . . . . 14 ⊢ ((𝜏 ∧ 𝑛 ∈ 𝐷) → (((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)) → 𝑔 ∈ 𝑤))
45	44	expimpd 453	. . . . . . . . . . . . 13 ⊢ (𝜏 → ((𝑛 ∈ 𝐷 ∧ ((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → 𝑔 ∈ 𝑤))
46	14, 45	biimtrid 242	. . . . . . . . . . . 12 ⊢ (𝜏 → (((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → 𝑔 ∈ 𝑤))
47	46	exlimdv 1932	. . . . . . . . . . 11 ⊢ (𝜏 → (∃𝑛((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ (𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → 𝑔 ∈ 𝑤))
48	13, 47	syl5 34	. . . . . . . . . 10 ⊢ (𝜏 → ((∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ∧ ∃𝑛(𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))) → 𝑔 ∈ 𝑤))
49	48	expdimp 452	. . . . . . . . 9 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → (∃𝑛(𝑛 ∈ 𝐷 ∧ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)) → 𝑔 ∈ 𝑤))
50	12, 49	biimtrid 242	. . . . . . . 8 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → (∃𝑛 ∈ 𝐷 (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′) → 𝑔 ∈ 𝑤))
51	50	abssdv 4067	. . . . . . 7 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → {𝑔 ∣ ∃𝑛 ∈ 𝐷 (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)} ⊆ 𝑤)
52	11, 51	eqsstrid 4021	. . . . . 6 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → 𝐵 ⊆ 𝑤)
53		vex 3483	. . . . . . 7 ⊢ 𝑤 ∈ V
54	53	ssex 5320	. . . . . 6 ⊢ (𝐵 ⊆ 𝑤 → 𝐵 ∈ V)
55	52, 54	syl 17	. . . . 5 ⊢ ((𝜏 ∧ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)) → 𝐵 ∈ V)
56	55	ex 412	. . . 4 ⊢ (𝜏 → (∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) → 𝐵 ∈ V))
57	56	exlimdv 1932	. . 3 ⊢ (𝜏 → (∃𝑤∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) → 𝐵 ∈ V))
58	7, 57	mpi 20	. 2 ⊢ (𝜏 → 𝐵 ∈ V)
59	1, 58	sylbir 235	1 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ∈ V)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086  ∀wal 1537   = wceq 1539  ∃wex 1778   ∈ wcel 2107  ∃!weu 2567  {cab 2713  ∀wral 3060  ∃wrex 3069  Vcvv 3479  [wsbc 3787   ∖ cdif 3947   ⊆ wss 3950  ∅c0 4332  {csn 4625  ∪ ciun 4990  suc csuc 6385   Fn wfn 6555  ‘cfv 6560  ωcom 7888   predc-bnj14 34703   FrSe w-bnj15 34707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-reg 9633  ax-inf2 9682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-om 7889  df-1o 8507  df-bnj17 34702  df-bnj14 34704  df-bnj13 34706  df-bnj15 34708

This theorem is referenced by:  bnj893  34943