This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elmptrab

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

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

Proof

Step Hyp Ref Expression
1 elmptrab.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } )
2 elmptrab.s1 ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝜑 ↔ 𝜓 ) )
3 elmptrab.s2 ⊢ ( 𝑥 = 𝑋 → 𝐵 = 𝐶 )
4 elmptrab.ex ⊢ ( 𝑥 ∈ 𝐷 → 𝐵 ∈ 𝑉 )
5 1 mptrcl ⊢ ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → 𝑋 ∈ 𝐷 )
6 simp1 ⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓 ) → 𝑋 ∈ 𝐷 )
7 csbeq1 ⊢ ( 𝑧 = 𝑋 → ⦋ 𝑧 / 𝑥 ⦌ 𝐵 = ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
8 dfsbcq ⊢ ( 𝑧 = 𝑋 → ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) )
9 7 8 rabeqbidv ⊢ ( 𝑧 = 𝑋 → { 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∣ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } = { 𝑤 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∣ [ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } )
10 nfcv ⊢ Ⅎ 𝑧 { 𝑦 ∈ 𝐵 ∣ 𝜑 }
11 nfsbc1v ⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑
12 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐵
13 11 12 nfrabw ⊢ Ⅎ 𝑥 { 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∣ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 }
14 csbeq1a ⊢ ( 𝑥 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
15 sbceq1a ⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
16 14 15 rabeqbidv ⊢ ( 𝑥 = 𝑧 → { 𝑦 ∈ 𝐵 ∣ 𝜑 } = { 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∣ [ 𝑧 / 𝑥 ] 𝜑 } )
17 nfcv ⊢ Ⅎ 𝑤 ⦋ 𝑧 / 𝑥 ⦌ 𝐵
18 nfcv ⊢ Ⅎ 𝑦 ⦋ 𝑧 / 𝑥 ⦌ 𝐵
19 nfcv ⊢ Ⅎ 𝑦 𝑧
20 nfsbc1v ⊢ Ⅎ 𝑦 [ 𝑤 / 𝑦 ] 𝜑
21 19 20 nfsbcw ⊢ Ⅎ 𝑦 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑
22 nfv ⊢ Ⅎ 𝑤 [ 𝑧 / 𝑥 ] 𝜑
23 sbccom ⊢ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 )
24 sbceq1a ⊢ ( 𝑦 = 𝑤 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 ) )
25 24 equcoms ⊢ ( 𝑤 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 ) )
26 23 25 bitr4id ⊢ ( 𝑤 = 𝑦 → ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
27 17 18 21 22 26 cbvrabw ⊢ { 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∣ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } = { 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∣ [ 𝑧 / 𝑥 ] 𝜑 }
28 16 27 eqtr4di ⊢ ( 𝑥 = 𝑧 → { 𝑦 ∈ 𝐵 ∣ 𝜑 } = { 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∣ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } )
29 10 13 28 cbvmpt ⊢ ( 𝑥 ∈ 𝐷 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) = ( 𝑧 ∈ 𝐷 ↦ { 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∣ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } )
30 1 29 eqtri ⊢ 𝐹 = ( 𝑧 ∈ 𝐷 ↦ { 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∣ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } )
31 nfv ⊢ Ⅎ 𝑥 𝑧 ∈ 𝐷
32 12 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ 𝑉
33 31 32 nfim ⊢ Ⅎ 𝑥 ( 𝑧 ∈ 𝐷 → ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ 𝑉 )
34 eleq1w ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷 ) )
35 14 eleq1d ⊢ ( 𝑥 = 𝑧 → ( 𝐵 ∈ 𝑉 ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ 𝑉 ) )
36 34 35 imbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐷 → 𝐵 ∈ 𝑉 ) ↔ ( 𝑧 ∈ 𝐷 → ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ 𝑉 ) ) )
37 33 36 4 chvarfv ⊢ ( 𝑧 ∈ 𝐷 → ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ 𝑉 )
38 rabexg ⊢ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ 𝑉 → { 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∣ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } ∈ V )
39 37 38 syl ⊢ ( 𝑧 ∈ 𝐷 → { 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∣ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } ∈ V )
40 9 30 39 fvmpt3 ⊢ ( 𝑋 ∈ 𝐷 → ( 𝐹 ‘ 𝑋 ) = { 𝑤 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∣ [ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } )
41 40 eleq2d ⊢ ( 𝑋 ∈ 𝐷 → ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) ↔ 𝑌 ∈ { 𝑤 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∣ [ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } ) )
42 dfsbcq ⊢ ( 𝑤 = 𝑌 → ( [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑌 / 𝑦 ] 𝜑 ) )
43 42 sbcbidv ⊢ ( 𝑤 = 𝑌 → ( [ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) )
44 43 elrab ⊢ ( 𝑌 ∈ { 𝑤 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∣ [ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } ↔ ( 𝑌 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∧ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) )
45 44 a1i ⊢ ( 𝑋 ∈ 𝐷 → ( 𝑌 ∈ { 𝑤 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∣ [ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } ↔ ( 𝑌 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∧ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) ) )
46 nfcvd ⊢ ( 𝑋 ∈ 𝐷 → Ⅎ 𝑥 𝐶 )
47 46 3 csbiegf ⊢ ( 𝑋 ∈ 𝐷 → ⦋ 𝑋 / 𝑥 ⦌ 𝐵 = 𝐶 )
48 47 eleq2d ⊢ ( 𝑋 ∈ 𝐷 → ( 𝑌 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ↔ 𝑌 ∈ 𝐶 ) )
49 48 anbi1d ⊢ ( 𝑋 ∈ 𝐷 → ( ( 𝑌 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∧ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) ↔ ( 𝑌 ∈ 𝐶 ∧ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) ) )
50 nfv ⊢ Ⅎ 𝑥 𝜓
51 nfv ⊢ Ⅎ 𝑦 𝜓
52 nfv ⊢ Ⅎ 𝑥 𝑌 ∈ 𝐶
53 50 51 52 2 sbc2iegf ⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ) → ( [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ↔ 𝜓 ) )
54 53 pm5.32da ⊢ ( 𝑋 ∈ 𝐷 → ( ( 𝑌 ∈ 𝐶 ∧ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) ↔ ( 𝑌 ∈ 𝐶 ∧ 𝜓 ) ) )
55 45 49 54 3bitrd ⊢ ( 𝑋 ∈ 𝐷 → ( 𝑌 ∈ { 𝑤 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∣ [ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } ↔ ( 𝑌 ∈ 𝐶 ∧ 𝜓 ) ) )
56 3anass ⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓 ) ↔ ( 𝑋 ∈ 𝐷 ∧ ( 𝑌 ∈ 𝐶 ∧ 𝜓 ) ) )
57 56 baibr ⊢ ( 𝑋 ∈ 𝐷 → ( ( 𝑌 ∈ 𝐶 ∧ 𝜓 ) ↔ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓 ) ) )
58 41 55 57 3bitrd ⊢ ( 𝑋 ∈ 𝐷 → ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) ↔ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓 ) ) )
59 5 6 58 pm5.21nii ⊢ ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) ↔ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓 ) )