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

Metamath Proof Explorer

Theorem prodindf

Description: The product of indicators is one if and only if all values are in the set. (Contributed by Thierry Arnoux, 11-Dec-2021)

Ref Expression
Hypotheses prodindf.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
prodindf.2 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
prodindf.3 ⊢ ( 𝜑 → 𝐵 ⊆ 𝑂 )
prodindf.4 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑂 )
Assertion prodindf ( 𝜑 → ∏ 𝑘 ∈ 𝐴 ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = if ( ran 𝐹 ⊆ 𝐵 , 1 , 0 ) )

Proof

Step Hyp Ref Expression
1 prodindf.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2 prodindf.2 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
3 prodindf.3 ⊢ ( 𝜑 → 𝐵 ⊆ 𝑂 )
4 prodindf.4 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑂 )
5 2fveq3 ⊢ ( 𝑘 = 𝑙 → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ ( 𝐹 ‘ 𝑙 ) ) )
6 indf ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐵 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) : 𝑂 ⟶ { 0 , 1 } )
7 1 3 6 syl2anc ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) : 𝑂 ⟶ { 0 , 1 } )
8 7 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) : 𝑂 ⟶ { 0 , 1 } )
9 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑂 )
10 8 9 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ { 0 , 1 } )
11 5 2 10 fprodex01 ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = if ( ∀ 𝑙 ∈ 𝐴 ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ ( 𝐹 ‘ 𝑙 ) ) = 1 , 1 , 0 ) )
12 2fveq3 ⊢ ( 𝑙 = 𝑘 → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ ( 𝐹 ‘ 𝑙 ) ) = ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ ( 𝐹 ‘ 𝑘 ) ) )
13 12 eqeq1d ⊢ ( 𝑙 = 𝑘 → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ ( 𝐹 ‘ 𝑙 ) ) = 1 ↔ ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = 1 ) )
14 13 cbvralvw ⊢ ( ∀ 𝑙 ∈ 𝐴 ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ ( 𝐹 ‘ 𝑙 ) ) = 1 ↔ ∀ 𝑘 ∈ 𝐴 ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = 1 )
15 14 a1i ⊢ ( 𝜑 → ( ∀ 𝑙 ∈ 𝐴 ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ ( 𝐹 ‘ 𝑙 ) ) = 1 ↔ ∀ 𝑘 ∈ 𝐴 ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = 1 ) )
16 15 ifbid ⊢ ( 𝜑 → if ( ∀ 𝑙 ∈ 𝐴 ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ ( 𝐹 ‘ 𝑙 ) ) = 1 , 1 , 0 ) = if ( ∀ 𝑘 ∈ 𝐴 ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = 1 , 1 , 0 ) )
17 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) )
18 17 rnmptss ⊢ ( ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 → ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ⊆ 𝐵 )
19 nfv ⊢ Ⅎ 𝑘 𝜑
20 nfmpt1 ⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) )
21 20 nfrn ⊢ Ⅎ 𝑘 ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) )
22 nfcv ⊢ Ⅎ 𝑘 𝐵
23 21 22 nfss ⊢ Ⅎ 𝑘 ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ⊆ 𝐵
24 19 23 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ⊆ 𝐵 )
25 simplr ⊢ ( ( ( 𝜑 ∧ ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ⊆ 𝐵 ) ∧ 𝑘 ∈ 𝐴 ) → ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ⊆ 𝐵 )
26 4 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) )
27 eqidd ⊢ ( 𝜑 → 𝑘 = 𝑘 )
28 26 27 fveq12d ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑘 ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑘 ) )
29 28 ralrimivw ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑘 ) )
30 29 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑘 ) )
31 4 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
32 26 fneq1d ⊢ ( 𝜑 → ( 𝐹 Fn 𝐴 ↔ ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) Fn 𝐴 ) )
33 31 32 mpbid ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) Fn 𝐴 )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) Fn 𝐴 )
35 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝐴 )
36 fnfvelrn ⊢ ( ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) Fn 𝐴 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑘 ) ∈ ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) )
37 34 35 36 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑘 ) ∈ ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) )
38 30 37 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) )
39 38 adantlr ⊢ ( ( ( 𝜑 ∧ ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ⊆ 𝐵 ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) )
40 25 39 sseldd ⊢ ( ( ( 𝜑 ∧ ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ⊆ 𝐵 ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 )
41 40 ex ⊢ ( ( 𝜑 ∧ ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ⊆ 𝐵 ) → ( 𝑘 ∈ 𝐴 → ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 ) )
42 24 41 ralrimi ⊢ ( ( 𝜑 ∧ ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ⊆ 𝐵 ) → ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 )
43 42 ex ⊢ ( 𝜑 → ( ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ⊆ 𝐵 → ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 ) )
44 18 43 impbid2 ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 ↔ ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ⊆ 𝐵 ) )
45 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑂 ∈ 𝑉 )
46 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ⊆ 𝑂 )
47 ind1a ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐵 ⊆ 𝑂 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑂 ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = 1 ↔ ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 ) )
48 45 46 9 47 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = 1 ↔ ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 ) )
49 48 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ 𝐴 ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = 1 ↔ ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 ) )
50 26 rneqd ⊢ ( 𝜑 → ran 𝐹 = ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) )
51 50 sseq1d ⊢ ( 𝜑 → ( ran 𝐹 ⊆ 𝐵 ↔ ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ⊆ 𝐵 ) )
52 44 49 51 3bitr4d ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ 𝐴 ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = 1 ↔ ran 𝐹 ⊆ 𝐵 ) )
53 52 ifbid ⊢ ( 𝜑 → if ( ∀ 𝑘 ∈ 𝐴 ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = 1 , 1 , 0 ) = if ( ran 𝐹 ⊆ 𝐵 , 1 , 0 ) )
54 11 16 53 3eqtrd ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = if ( ran 𝐹 ⊆ 𝐵 , 1 , 0 ) )