Metamath Proof Explorer


Theorem pw2f1olem

Description: Lemma for pw2f1o . (Contributed by Mario Carneiro, 6-Oct-2014)

Ref Expression
Hypotheses pw2f1o.1 ( 𝜑𝐴𝑉 )
pw2f1o.2 ( 𝜑𝐵𝑊 )
pw2f1o.3 ( 𝜑𝐶𝑊 )
pw2f1o.4 ( 𝜑𝐵𝐶 )
Assertion pw2f1olem ( 𝜑 → ( ( 𝑆 ∈ 𝒫 𝐴𝐺 = ( 𝑧𝐴 ↦ if ( 𝑧𝑆 , 𝐶 , 𝐵 ) ) ) ↔ ( 𝐺 ∈ ( { 𝐵 , 𝐶 } ↑m 𝐴 ) ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) )

Proof

Step Hyp Ref Expression
1 pw2f1o.1 ( 𝜑𝐴𝑉 )
2 pw2f1o.2 ( 𝜑𝐵𝑊 )
3 pw2f1o.3 ( 𝜑𝐶𝑊 )
4 pw2f1o.4 ( 𝜑𝐵𝐶 )
5 prid2g ( 𝐶𝑊𝐶 ∈ { 𝐵 , 𝐶 } )
6 3 5 syl ( 𝜑𝐶 ∈ { 𝐵 , 𝐶 } )
7 prid1g ( 𝐵𝑊𝐵 ∈ { 𝐵 , 𝐶 } )
8 2 7 syl ( 𝜑𝐵 ∈ { 𝐵 , 𝐶 } )
9 6 8 ifcld ( 𝜑 → if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ∈ { 𝐵 , 𝐶 } )
10 9 adantr ( ( 𝜑𝑦𝐴 ) → if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ∈ { 𝐵 , 𝐶 } )
11 10 fmpttd ( 𝜑 → ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) : 𝐴 ⟶ { 𝐵 , 𝐶 } )
12 11 adantr ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) → ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) : 𝐴 ⟶ { 𝐵 , 𝐶 } )
13 simprr ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) → 𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) )
14 13 feq1d ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) → ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ↔ ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) : 𝐴 ⟶ { 𝐵 , 𝐶 } ) )
15 12 14 mpbird ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) → 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } )
16 iftrue ( 𝑥𝑆 → if ( 𝑥𝑆 , 𝐶 , 𝐵 ) = 𝐶 )
17 4 ad2antrr ( ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) ∧ 𝑥𝐴 ) → 𝐵𝐶 )
18 iffalse ( ¬ 𝑥𝑆 → if ( 𝑥𝑆 , 𝐶 , 𝐵 ) = 𝐵 )
19 18 neeq1d ( ¬ 𝑥𝑆 → ( if ( 𝑥𝑆 , 𝐶 , 𝐵 ) ≠ 𝐶𝐵𝐶 ) )
20 17 19 syl5ibrcom ( ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) ∧ 𝑥𝐴 ) → ( ¬ 𝑥𝑆 → if ( 𝑥𝑆 , 𝐶 , 𝐵 ) ≠ 𝐶 ) )
21 20 necon4bd ( ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) ∧ 𝑥𝐴 ) → ( if ( 𝑥𝑆 , 𝐶 , 𝐵 ) = 𝐶𝑥𝑆 ) )
22 16 21 impbid2 ( ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) ∧ 𝑥𝐴 ) → ( 𝑥𝑆 ↔ if ( 𝑥𝑆 , 𝐶 , 𝐵 ) = 𝐶 ) )
23 simplrr ( ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) ∧ 𝑥𝐴 ) → 𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) )
24 23 fveq1d ( ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) ∧ 𝑥𝐴 ) → ( 𝐺𝑥 ) = ( ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ‘ 𝑥 ) )
25 id ( 𝑥𝐴𝑥𝐴 )
26 6 8 ifcld ( 𝜑 → if ( 𝑥𝑆 , 𝐶 , 𝐵 ) ∈ { 𝐵 , 𝐶 } )
27 26 adantr ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) → if ( 𝑥𝑆 , 𝐶 , 𝐵 ) ∈ { 𝐵 , 𝐶 } )
28 eleq1w ( 𝑦 = 𝑥 → ( 𝑦𝑆𝑥𝑆 ) )
29 28 ifbid ( 𝑦 = 𝑥 → if ( 𝑦𝑆 , 𝐶 , 𝐵 ) = if ( 𝑥𝑆 , 𝐶 , 𝐵 ) )
30 eqid ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) )
31 29 30 fvmptg ( ( 𝑥𝐴 ∧ if ( 𝑥𝑆 , 𝐶 , 𝐵 ) ∈ { 𝐵 , 𝐶 } ) → ( ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ‘ 𝑥 ) = if ( 𝑥𝑆 , 𝐶 , 𝐵 ) )
32 25 27 31 syl2anr ( ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) ∧ 𝑥𝐴 ) → ( ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ‘ 𝑥 ) = if ( 𝑥𝑆 , 𝐶 , 𝐵 ) )
33 24 32 eqtrd ( ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) ∧ 𝑥𝐴 ) → ( 𝐺𝑥 ) = if ( 𝑥𝑆 , 𝐶 , 𝐵 ) )
34 33 eqeq1d ( ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) ∧ 𝑥𝐴 ) → ( ( 𝐺𝑥 ) = 𝐶 ↔ if ( 𝑥𝑆 , 𝐶 , 𝐵 ) = 𝐶 ) )
35 22 34 bitr4d ( ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) ∧ 𝑥𝐴 ) → ( 𝑥𝑆 ↔ ( 𝐺𝑥 ) = 𝐶 ) )
36 35 pm5.32da ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) → ( ( 𝑥𝐴𝑥𝑆 ) ↔ ( 𝑥𝐴 ∧ ( 𝐺𝑥 ) = 𝐶 ) ) )
37 simprl ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) → 𝑆𝐴 )
38 37 sseld ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) → ( 𝑥𝑆𝑥𝐴 ) )
39 38 pm4.71rd ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) → ( 𝑥𝑆 ↔ ( 𝑥𝐴𝑥𝑆 ) ) )
40 ffn ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } → 𝐺 Fn 𝐴 )
41 15 40 syl ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) → 𝐺 Fn 𝐴 )
42 fniniseg ( 𝐺 Fn 𝐴 → ( 𝑥 ∈ ( 𝐺 “ { 𝐶 } ) ↔ ( 𝑥𝐴 ∧ ( 𝐺𝑥 ) = 𝐶 ) ) )
43 41 42 syl ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) → ( 𝑥 ∈ ( 𝐺 “ { 𝐶 } ) ↔ ( 𝑥𝐴 ∧ ( 𝐺𝑥 ) = 𝐶 ) ) )
44 36 39 43 3bitr4d ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) → ( 𝑥𝑆𝑥 ∈ ( 𝐺 “ { 𝐶 } ) ) )
45 44 eqrdv ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) → 𝑆 = ( 𝐺 “ { 𝐶 } ) )
46 15 45 jca ( ( 𝜑 ∧ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) → ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) )
47 simprr ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) → 𝑆 = ( 𝐺 “ { 𝐶 } ) )
48 cnvimass ( 𝐺 “ { 𝐶 } ) ⊆ dom 𝐺
49 fdm ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } → dom 𝐺 = 𝐴 )
50 49 ad2antrl ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) → dom 𝐺 = 𝐴 )
51 48 50 sseqtrid ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) → ( 𝐺 “ { 𝐶 } ) ⊆ 𝐴 )
52 47 51 eqsstrd ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) → 𝑆𝐴 )
53 40 ad2antrl ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) → 𝐺 Fn 𝐴 )
54 dffn5 ( 𝐺 Fn 𝐴𝐺 = ( 𝑦𝐴 ↦ ( 𝐺𝑦 ) ) )
55 53 54 sylib ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) → 𝐺 = ( 𝑦𝐴 ↦ ( 𝐺𝑦 ) ) )
56 simplrr ( ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) ∧ 𝑦𝐴 ) → 𝑆 = ( 𝐺 “ { 𝐶 } ) )
57 56 eleq2d ( ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) ∧ 𝑦𝐴 ) → ( 𝑦𝑆𝑦 ∈ ( 𝐺 “ { 𝐶 } ) ) )
58 fniniseg ( 𝐺 Fn 𝐴 → ( 𝑦 ∈ ( 𝐺 “ { 𝐶 } ) ↔ ( 𝑦𝐴 ∧ ( 𝐺𝑦 ) = 𝐶 ) ) )
59 53 58 syl ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) → ( 𝑦 ∈ ( 𝐺 “ { 𝐶 } ) ↔ ( 𝑦𝐴 ∧ ( 𝐺𝑦 ) = 𝐶 ) ) )
60 59 baibd ( ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) ∧ 𝑦𝐴 ) → ( 𝑦 ∈ ( 𝐺 “ { 𝐶 } ) ↔ ( 𝐺𝑦 ) = 𝐶 ) )
61 57 60 bitrd ( ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) ∧ 𝑦𝐴 ) → ( 𝑦𝑆 ↔ ( 𝐺𝑦 ) = 𝐶 ) )
62 61 biimpa ( ( ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) ∧ 𝑦𝐴 ) ∧ 𝑦𝑆 ) → ( 𝐺𝑦 ) = 𝐶 )
63 iftrue ( 𝑦𝑆 → if ( 𝑦𝑆 , 𝐶 , 𝐵 ) = 𝐶 )
64 63 adantl ( ( ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) ∧ 𝑦𝐴 ) ∧ 𝑦𝑆 ) → if ( 𝑦𝑆 , 𝐶 , 𝐵 ) = 𝐶 )
65 62 64 eqtr4d ( ( ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) ∧ 𝑦𝐴 ) ∧ 𝑦𝑆 ) → ( 𝐺𝑦 ) = if ( 𝑦𝑆 , 𝐶 , 𝐵 ) )
66 simprl ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) → 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } )
67 66 ffvelrnda ( ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) ∧ 𝑦𝐴 ) → ( 𝐺𝑦 ) ∈ { 𝐵 , 𝐶 } )
68 fvex ( 𝐺𝑦 ) ∈ V
69 68 elpr ( ( 𝐺𝑦 ) ∈ { 𝐵 , 𝐶 } ↔ ( ( 𝐺𝑦 ) = 𝐵 ∨ ( 𝐺𝑦 ) = 𝐶 ) )
70 67 69 sylib ( ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) ∧ 𝑦𝐴 ) → ( ( 𝐺𝑦 ) = 𝐵 ∨ ( 𝐺𝑦 ) = 𝐶 ) )
71 70 ord ( ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) ∧ 𝑦𝐴 ) → ( ¬ ( 𝐺𝑦 ) = 𝐵 → ( 𝐺𝑦 ) = 𝐶 ) )
72 71 61 sylibrd ( ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) ∧ 𝑦𝐴 ) → ( ¬ ( 𝐺𝑦 ) = 𝐵𝑦𝑆 ) )
73 72 con1d ( ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) ∧ 𝑦𝐴 ) → ( ¬ 𝑦𝑆 → ( 𝐺𝑦 ) = 𝐵 ) )
74 73 imp ( ( ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) ∧ 𝑦𝐴 ) ∧ ¬ 𝑦𝑆 ) → ( 𝐺𝑦 ) = 𝐵 )
75 iffalse ( ¬ 𝑦𝑆 → if ( 𝑦𝑆 , 𝐶 , 𝐵 ) = 𝐵 )
76 75 adantl ( ( ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) ∧ 𝑦𝐴 ) ∧ ¬ 𝑦𝑆 ) → if ( 𝑦𝑆 , 𝐶 , 𝐵 ) = 𝐵 )
77 74 76 eqtr4d ( ( ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) ∧ 𝑦𝐴 ) ∧ ¬ 𝑦𝑆 ) → ( 𝐺𝑦 ) = if ( 𝑦𝑆 , 𝐶 , 𝐵 ) )
78 65 77 pm2.61dan ( ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) ∧ 𝑦𝐴 ) → ( 𝐺𝑦 ) = if ( 𝑦𝑆 , 𝐶 , 𝐵 ) )
79 78 mpteq2dva ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) → ( 𝑦𝐴 ↦ ( 𝐺𝑦 ) ) = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) )
80 55 79 eqtrd ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) → 𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) )
81 52 80 jca ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) → ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) )
82 46 81 impbida ( 𝜑 → ( ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ↔ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) )
83 elpw2g ( 𝐴𝑉 → ( 𝑆 ∈ 𝒫 𝐴𝑆𝐴 ) )
84 1 83 syl ( 𝜑 → ( 𝑆 ∈ 𝒫 𝐴𝑆𝐴 ) )
85 eleq1w ( 𝑧 = 𝑦 → ( 𝑧𝑆𝑦𝑆 ) )
86 85 ifbid ( 𝑧 = 𝑦 → if ( 𝑧𝑆 , 𝐶 , 𝐵 ) = if ( 𝑦𝑆 , 𝐶 , 𝐵 ) )
87 86 cbvmptv ( 𝑧𝐴 ↦ if ( 𝑧𝑆 , 𝐶 , 𝐵 ) ) = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) )
88 87 a1i ( 𝜑 → ( 𝑧𝐴 ↦ if ( 𝑧𝑆 , 𝐶 , 𝐵 ) ) = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) )
89 88 eqeq2d ( 𝜑 → ( 𝐺 = ( 𝑧𝐴 ↦ if ( 𝑧𝑆 , 𝐶 , 𝐵 ) ) ↔ 𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) )
90 84 89 anbi12d ( 𝜑 → ( ( 𝑆 ∈ 𝒫 𝐴𝐺 = ( 𝑧𝐴 ↦ if ( 𝑧𝑆 , 𝐶 , 𝐵 ) ) ) ↔ ( 𝑆𝐴𝐺 = ( 𝑦𝐴 ↦ if ( 𝑦𝑆 , 𝐶 , 𝐵 ) ) ) ) )
91 prex { 𝐵 , 𝐶 } ∈ V
92 elmapg ( ( { 𝐵 , 𝐶 } ∈ V ∧ 𝐴𝑉 ) → ( 𝐺 ∈ ( { 𝐵 , 𝐶 } ↑m 𝐴 ) ↔ 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ) )
93 91 1 92 sylancr ( 𝜑 → ( 𝐺 ∈ ( { 𝐵 , 𝐶 } ↑m 𝐴 ) ↔ 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ) )
94 93 anbi1d ( 𝜑 → ( ( 𝐺 ∈ ( { 𝐵 , 𝐶 } ↑m 𝐴 ) ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ↔ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) )
95 82 90 94 3bitr4d ( 𝜑 → ( ( 𝑆 ∈ 𝒫 𝐴𝐺 = ( 𝑧𝐴 ↦ if ( 𝑧𝑆 , 𝐶 , 𝐵 ) ) ) ↔ ( 𝐺 ∈ ( { 𝐵 , 𝐶 } ↑m 𝐴 ) ∧ 𝑆 = ( 𝐺 “ { 𝐶 } ) ) ) )