Theorem csbima12gALTVD 44259

Description: Virtual deduction proof of csbima12 6076. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. csbima12 6076 is csbima12gALTVD 44259 without virtual deductions and was automatically derived from csbima12gALTVD 44259.

1::	⊢ (   𝐴 ∈ 𝐶   ▶   𝐴 ∈ 𝐶   )
2:1:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵) = ( ⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵)   )
3:2:	⊢ (   𝐴 ∈ 𝐶   ▶    ran ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵)   )
4:1:	⊢ (   𝐴 ∈ 𝐶   ▶    ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) = ran ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵)   )
5:3,4:	⊢ (   𝐴 ∈ 𝐶   ▶    ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵)   )
6::	⊢ (𝐹 “ 𝐵) = ran (𝐹 ↾ 𝐵)
7:6:	⊢ ∀𝑥(𝐹 “ 𝐵) = ran (𝐹 ↾ 𝐵)
8:1,7:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ⦋ 𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵)   )
9:5,8:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵)   )
10::	⊢ (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵)
11:9,10:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ( ⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵)   )
qed:11:	⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = (⦋ 𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵))

(Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
csbima12gALTVD	⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵))

Proof of Theorem csbima12gALTVD

Step	Hyp	Ref	Expression
1		idn1 43936	. . . . . . 7 ⊢ (   𝐴 ∈ 𝐶   ▶   𝐴 ∈ 𝐶   )
2		csbres 5982	. . . . . . . 8 ⊢ ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵)
3	2	a1i 11	. . . . . . 7 ⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵))
4	1, 3	e1a 43989	. . . . . 6 ⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵)   )
5		rneq 5932	. . . . . 6 ⊢ (⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵) → ran ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵))
6	4, 5	e1a 43989	. . . . 5 ⊢ (   𝐴 ∈ 𝐶   ▶   ran ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵)   )
7		csbrn 6201	. . . . . . 7 ⊢ ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) = ran ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵)
8	7	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) = ran ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵))
9	1, 8	e1a 43989	. . . . 5 ⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) = ran ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵)   )
10		eqeq2 2739	. . . . . 6 ⊢ (ran ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵) → (⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) = ran ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵) ↔ ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵)))
11	10	biimpd 228	. . . . 5 ⊢ (ran ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵) → (⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) = ran ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵) → ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵)))
12	6, 9, 11	e11 44050	. . . 4 ⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵)   )
13		df-ima 5685	. . . . . 6 ⊢ (𝐹 “ 𝐵) = ran (𝐹 ↾ 𝐵)
14	13	ax-gen 1790	. . . . 5 ⊢ ∀𝑥(𝐹 “ 𝐵) = ran (𝐹 ↾ 𝐵)
15		csbeq2 3894	. . . . . 6 ⊢ (∀𝑥(𝐹 “ 𝐵) = ran (𝐹 ↾ 𝐵) → ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵))
16	15	a1i 11	. . . . 5 ⊢ (𝐴 ∈ 𝐶 → (∀𝑥(𝐹 “ 𝐵) = ran (𝐹 ↾ 𝐵) → ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵)))
17	1, 14, 16	e10 44056	. . . 4 ⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵)   )
18		eqeq2 2739	. . . . 5 ⊢ (⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵) → (⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) ↔ ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵)))
19	18	biimpd 228	. . . 4 ⊢ (⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵) → (⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) → ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵)))
20	12, 17, 19	e11 44050	. . 3 ⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵)   )
21		df-ima 5685	. . 3 ⊢ (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵)
22		eqeq2 2739	. . . 4 ⊢ ((⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵) → (⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵) ↔ ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵)))
23	22	biimprcd 249	. . 3 ⊢ (⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵) → ((⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵) → ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵)))
24	20, 21, 23	e10 44056	. 2 ⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵)   )
25	24	in1 43933	1 ⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵))

Syntax hints:   → wi 4  ∀wal 1532   = wceq 1534   ∈ wcel 2099  ⦋csb 3889  ran crn 5673   ↾ cres 5674   “ cima 5675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5143  df-opab 5205  df-xp 5678  df-rel 5679  df-cnv 5680  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-vd1 43932

This theorem is referenced by: (None)