Theorem bnj1015 35662

Description: Technical lemma for bnj69 35710. 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.) (New usage is discouraged.)

Hypotheses

Ref	Expression
bnj1015.1	⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))
bnj1015.2	⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))
bnj1015.13	⊢ 𝐷 = (ω ∖ {∅})
bnj1015.14	⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}
bnj1015.15	⊢ 𝐺 ∈ 𝑉
bnj1015.16	⊢ 𝐽 ∈ 𝑉

Assertion

Ref	Expression
bnj1015	⊢ ((𝐺 ∈ 𝐵 ∧ 𝐽 ∈ dom 𝐺) → (𝐺‘𝐽) ⊆ trCl(𝑋, 𝐴, 𝑅))

Distinct variable groups:   𝐴,𝑓,𝑖,𝑛,𝑦   𝐷,𝑖   𝑅,𝑓,𝑖,𝑛,𝑦   𝑓,𝑋,𝑖,𝑛,𝑦   𝜑,𝑖

Allowed substitution hints:   𝜑(𝑦, 𝑓, 𝑛)   𝜓(𝑦, 𝑓, 𝑖, 𝑛)   𝐵(𝑦, 𝑓, 𝑖, 𝑛)   𝐷(𝑦, 𝑓, 𝑛)   𝐺(𝑦, 𝑓, 𝑖, 𝑛)   𝐽(𝑦, 𝑓, 𝑖, 𝑛)   𝑉(𝑦, 𝑓, 𝑖, 𝑛)

Proof of Theorem bnj1015

Dummy variables 𝑔 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		bnj1015.16	. . 3 ⊢ 𝐽 ∈ 𝑉
2	1	elexi 3476	. 2 ⊢ 𝐽 ∈ V
3		eleq1 2852	. . . 4 ⊢ (𝑗 = 𝐽 → (𝑗 ∈ dom 𝐺 ↔ 𝐽 ∈ dom 𝐺))
4	3	anbi2d 642	. . 3 ⊢ (𝑗 = 𝐽 → ((𝐺 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝐺) ↔ (𝐺 ∈ 𝐵 ∧ 𝐽 ∈ dom 𝐺)))
5		fveq2 6908	. . . 4 ⊢ (𝑗 = 𝐽 → (𝐺‘𝑗) = (𝐺‘𝐽))
6	5	sseq1d 3944	. . 3 ⊢ (𝑗 = 𝐽 → ((𝐺‘𝑗) ⊆ trCl(𝑋, 𝐴, 𝑅) ↔ (𝐺‘𝐽) ⊆ trCl(𝑋, 𝐴, 𝑅)))
7	4, 6	imbi12d 347	. 2 ⊢ (𝑗 = 𝐽 → (((𝐺 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝐺) → (𝐺‘𝑗) ⊆ trCl(𝑋, 𝐴, 𝑅)) ↔ ((𝐺 ∈ 𝐵 ∧ 𝐽 ∈ dom 𝐺) → (𝐺‘𝐽) ⊆ trCl(𝑋, 𝐴, 𝑅))))
8		bnj1015.15	. . . 4 ⊢ 𝐺 ∈ 𝑉
9	8	elexi 3476	. . 3 ⊢ 𝐺 ∈ V
10		eleq1 2852	. . . . 5 ⊢ (𝑔 = 𝐺 → (𝑔 ∈ 𝐵 ↔ 𝐺 ∈ 𝐵))
11		dmeq 5892	. . . . . 6 ⊢ (𝑔 = 𝐺 → dom 𝑔 = dom 𝐺)
12	11	eleq2d 2850	. . . . 5 ⊢ (𝑔 = 𝐺 → (𝑗 ∈ dom 𝑔 ↔ 𝑗 ∈ dom 𝐺))
13	10, 12	anbi12d 644	. . . 4 ⊢ (𝑔 = 𝐺 → ((𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔) ↔ (𝐺 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝐺)))
14		fveq1 6907	. . . . 5 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑗) = (𝐺‘𝑗))
15	14	sseq1d 3944	. . . 4 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑗) ⊆ trCl(𝑋, 𝐴, 𝑅) ↔ (𝐺‘𝑗) ⊆ trCl(𝑋, 𝐴, 𝑅)))
16	13, 15	imbi12d 347	. . 3 ⊢ (𝑔 = 𝐺 → (((𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔) → (𝑔‘𝑗) ⊆ trCl(𝑋, 𝐴, 𝑅)) ↔ ((𝐺 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝐺) → (𝐺‘𝑗) ⊆ trCl(𝑋, 𝐴, 𝑅))))
17		bnj1015.1	. . . 4 ⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))
18		bnj1015.2	. . . 4 ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))
19		bnj1015.13	. . . 4 ⊢ 𝐷 = (ω ∖ {∅})
20		bnj1015.14	. . . 4 ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}
21	17, 18, 19, 20	bnj1014 35661	. . 3 ⊢ ((𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔) → (𝑔‘𝑗) ⊆ trCl(𝑋, 𝐴, 𝑅))
22	9, 16, 21	vtocl 3524	. 2 ⊢ ((𝐺 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝐺) → (𝐺‘𝑗) ⊆ trCl(𝑋, 𝐴, 𝑅))
23	2, 7, 22	vtocl 3524	1 ⊢ ((𝐺 ∈ 𝐵 ∧ 𝐽 ∈ dom 𝐺) → (𝐺‘𝐽) ⊆ trCl(𝑋, 𝐴, 𝑅))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  {cab 2741  ∀wral 3080  ∃wrex 3090   ⊆ wss 3900   ∖ cdif 4048  ∅c0 4281  {csn 4588  ∪ ciun 4954  dom cdm 5655  suc csuc 6382   Fn wfn 6553  ‘cfv 6558  ωcom 7901   predc-bnj14 35389   trClc-bnj18 35395

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-dm 5665  df-iota 6512  df-fv 6566  df-bnj18 35396

This theorem is used by:  bnj1018g  35663  bnj1018  35664