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⟼ifz∈SCB↔G∈BCA∧S=G-1C

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