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

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 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝐺 : 𝐴 ⟶ { 𝐵 , 𝐶 } ∧ 𝑆 = ( ◡ 𝐺 “ { 𝐶 } ) ) ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑦 ) ∈ { 𝐵 , 𝐶 } )
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 𝐴 ) ∧ 𝑆 = ( ◡ 𝐺 “ { 𝐶 } ) ) ) )