Metamath Proof Explorer

Theorem pw2f1olem

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

Ref Expression
Hypotheses pw2f1o.1 ⊢ φ → A ∈ V
pw2f1o.2 ⊢ φ → B ∈ W
pw2f1o.3 ⊢ φ → C ∈ W
pw2f1o.4 ⊢ φ → B ≠ C
Assertion pw2f1olem ⊢ φ → S ∈ 𝒫 A ∧ G = z ∈ A ⟼ if z ∈ S C B ↔ G ∈ B C A ∧ S = G -1 C

Proof

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