Description: Hypothesis builder for function operation. (Contributed by Mario Carneiro, 20-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Hypothesis | nfof.1 | ⊢ Ⅎ 𝑥 𝑅 | |
Assertion | nfof | ⊢ Ⅎ 𝑥 ∘f 𝑅 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfof.1 | ⊢ Ⅎ 𝑥 𝑅 | |
2 | df-of | ⊢ ∘f 𝑅 = ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ( 𝑤 ∈ ( dom 𝑢 ∩ dom 𝑣 ) ↦ ( ( 𝑢 ‘ 𝑤 ) 𝑅 ( 𝑣 ‘ 𝑤 ) ) ) ) | |
3 | nfcv | ⊢ Ⅎ 𝑥 V | |
4 | nfcv | ⊢ Ⅎ 𝑥 ( dom 𝑢 ∩ dom 𝑣 ) | |
5 | nfcv | ⊢ Ⅎ 𝑥 ( 𝑢 ‘ 𝑤 ) | |
6 | nfcv | ⊢ Ⅎ 𝑥 ( 𝑣 ‘ 𝑤 ) | |
7 | 5 1 6 | nfov | ⊢ Ⅎ 𝑥 ( ( 𝑢 ‘ 𝑤 ) 𝑅 ( 𝑣 ‘ 𝑤 ) ) |
8 | 4 7 | nfmpt | ⊢ Ⅎ 𝑥 ( 𝑤 ∈ ( dom 𝑢 ∩ dom 𝑣 ) ↦ ( ( 𝑢 ‘ 𝑤 ) 𝑅 ( 𝑣 ‘ 𝑤 ) ) ) |
9 | 3 3 8 | nfmpo | ⊢ Ⅎ 𝑥 ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ( 𝑤 ∈ ( dom 𝑢 ∩ dom 𝑣 ) ↦ ( ( 𝑢 ‘ 𝑤 ) 𝑅 ( 𝑣 ‘ 𝑤 ) ) ) ) |
10 | 2 9 | nfcxfr | ⊢ Ⅎ 𝑥 ∘f 𝑅 |