Theorem elmptrab 23894

Description: Membership in a one-parameter class of sets. (Contributed by Stefan O'Rear, 28-Jul-2015.)

Hypotheses

Ref	Expression
elmptrab.f	⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ 𝜑})
elmptrab.s1	⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝜑 ↔ 𝜓))
elmptrab.s2	⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶)
elmptrab.ex	⊢ (𝑥 ∈ 𝐷 → 𝐵 ∈ 𝑉)

Assertion

Ref	Expression
elmptrab	⊢ (𝑌 ∈ (𝐹‘𝑋) ↔ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓))

Distinct variable groups:   𝑥,𝑦,𝑋   𝑦,𝐵   𝑥,𝐶,𝑦   𝑥,𝐷   𝑥,𝑉,𝑦   𝑥,𝑌,𝑦   𝜓,𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐵(𝑥)   𝐷(𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem elmptrab

Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elmptrab.f	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ 𝜑})
2	1	mptrcl 6985	. 2 ⊢ (𝑌 ∈ (𝐹‘𝑋) → 𝑋 ∈ 𝐷)
3		simp1 1150	. 2 ⊢ ((𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓) → 𝑋 ∈ 𝐷)
4		csbeq1 3856	. . . . . 6 ⊢ (𝑧 = 𝑋 → ⦋𝑧 / 𝑥⦌𝐵 = ⦋𝑋 / 𝑥⦌𝐵)
5		dfsbcq 3747	. . . . . 6 ⊢ (𝑧 = 𝑋 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑))
6	4, 5	rabeqbidv 3433	. . . . 5 ⊢ (𝑧 = 𝑋 → {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑} = {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑})
7		nfcv 2925	. . . . . . 7 ⊢ Ⅎ𝑧{𝑦 ∈ 𝐵 ∣ 𝜑}
8		nfsbc1v 3765	. . . . . . . 8 ⊢ Ⅎ𝑥[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
9		nfcsb1v 3877	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵
10	8, 9	nfrabw 3452	. . . . . . 7 ⊢ Ⅎ𝑥{𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑}
11		csbeq1a 3867	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵)
12		sbceq1a 3756	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
13	11, 12	rabeqbidv 3433	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥]𝜑})
14		nfcv 2925	. . . . . . . . 9 ⊢ Ⅎ𝑤⦋𝑧 / 𝑥⦌𝐵
15		nfcv 2925	. . . . . . . . 9 ⊢ Ⅎ𝑦⦋𝑧 / 𝑥⦌𝐵
16		nfcv 2925	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝑧
17		nfsbc1v 3765	. . . . . . . . . 10 ⊢ Ⅎ𝑦[𝑤 / 𝑦]𝜑
18	16, 17	nfsbcw 3767	. . . . . . . . 9 ⊢ Ⅎ𝑦[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
19		nfv 1935	. . . . . . . . 9 ⊢ Ⅎ𝑤[𝑧 / 𝑥]𝜑
20		sbccom 3825	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑)
21		sbceq1a 3756	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑤 → ([𝑧 / 𝑥]𝜑 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑))
22	21	equcoms 2041	. . . . . . . . . 10 ⊢ (𝑤 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑))
23	20, 22	bitr4id 292	. . . . . . . . 9 ⊢ (𝑤 = 𝑦 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑧 / 𝑥]𝜑))
24	14, 15, 18, 19, 23	cbvrabw 3450	. . . . . . . 8 ⊢ {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑} = {𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥]𝜑}
25	13, 24	eqtr4di 2816	. . . . . . 7 ⊢ (𝑥 = 𝑧 → {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑})
26	7, 10, 25	cbvmpt 5203	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ 𝜑}) = (𝑧 ∈ 𝐷 ↦ {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑})
27	1, 26	eqtri 2786	. . . . 5 ⊢ 𝐹 = (𝑧 ∈ 𝐷 ↦ {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑})
28		nfv 1935	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐷
29	9	nfel1 2941	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉
30	28, 29	nfim 1917	. . . . . . 7 ⊢ Ⅎ𝑥(𝑧 ∈ 𝐷 → ⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉)
31		eleq1w 2846	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷))
32	11	eleq1d 2848	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝐵 ∈ 𝑉 ↔ ⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉))
33	31, 32	imbi12d 346	. . . . . . 7 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐷 → 𝐵 ∈ 𝑉) ↔ (𝑧 ∈ 𝐷 → ⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉)))
34		elmptrab.ex	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → 𝐵 ∈ 𝑉)
35	30, 33, 34	chvarfv 2276	. . . . . 6 ⊢ (𝑧 ∈ 𝐷 → ⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉)
36		rabexg 5294	. . . . . 6 ⊢ (⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉 → {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑} ∈ V)
37	35, 36	syl 17	. . . . 5 ⊢ (𝑧 ∈ 𝐷 → {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑} ∈ V)
38	6, 27, 37	fvmpt3 6980	. . . 4 ⊢ (𝑋 ∈ 𝐷 → (𝐹‘𝑋) = {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑})
39	38	eleq2d 2849	. . 3 ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ (𝐹‘𝑋) ↔ 𝑌 ∈ {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑}))
40		dfsbcq 3747	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ([𝑤 / 𝑦]𝜑 ↔ [𝑌 / 𝑦]𝜑))
41	40	sbcbidv 3800	. . . . . 6 ⊢ (𝑤 = 𝑌 → ([𝑋 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑))
42	41	elrab 3651	. . . . 5 ⊢ (𝑌 ∈ {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑} ↔ (𝑌 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑))
43	42	a1i 11	. . . 4 ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑} ↔ (𝑌 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑)))
44		nfcvd 2926	. . . . . . 7 ⊢ (𝑋 ∈ 𝐷 → Ⅎ𝑥𝐶)
45		elmptrab.s2	. . . . . . 7 ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶)
46	44, 45	csbiegf 3886	. . . . . 6 ⊢ (𝑋 ∈ 𝐷 → ⦋𝑋 / 𝑥⦌𝐵 = 𝐶)
47	46	eleq2d 2849	. . . . 5 ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ ⦋𝑋 / 𝑥⦌𝐵 ↔ 𝑌 ∈ 𝐶))
48	47	anbi1d 640	. . . 4 ⊢ (𝑋 ∈ 𝐷 → ((𝑌 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑) ↔ (𝑌 ∈ 𝐶 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑)))
49		nfv 1935	. . . . . 6 ⊢ Ⅎ𝑥𝜓
50		nfv 1935	. . . . . 6 ⊢ Ⅎ𝑦𝜓
51		nfv 1935	. . . . . 6 ⊢ Ⅎ𝑥 𝑌 ∈ 𝐶
52		elmptrab.s1	. . . . . 6 ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝜑 ↔ 𝜓))
53	49, 50, 51, 52	sbc2iegf 3819	. . . . 5 ⊢ ((𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶) → ([𝑋 / 𝑥][𝑌 / 𝑦]𝜑 ↔ 𝜓))
54	53	pm5.32da 587	. . . 4 ⊢ (𝑋 ∈ 𝐷 → ((𝑌 ∈ 𝐶 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑) ↔ (𝑌 ∈ 𝐶 ∧ 𝜓)))
55	43, 48, 54	3bitrd 307	. . 3 ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑} ↔ (𝑌 ∈ 𝐶 ∧ 𝜓)))
56		3anass 1107	. . . 4 ⊢ ((𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓) ↔ (𝑋 ∈ 𝐷 ∧ (𝑌 ∈ 𝐶 ∧ 𝜓)))
57	56	baibr 544	. . 3 ⊢ (𝑋 ∈ 𝐷 → ((𝑌 ∈ 𝐶 ∧ 𝜓) ↔ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓)))
58	39, 55, 57	3bitrd 307	. 2 ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ (𝐹‘𝑋) ↔ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓)))
59	2, 3, 58	pm5.21nii 380	1 ⊢ (𝑌 ∈ (𝐹‘𝑋) ↔ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∧ w3a 1099   = wceq 1561   ∈ wcel 2143  {crab 3415  Vcvv 3455  [wsbc 3745  ⦋csb 3853   ↦ cmpt 5182  ‘cfv 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pr 5391

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6477  df-fun 6523  df-fv 6529

This theorem is referenced by:  elmptrab2  23895  isfbas  23896