definition powerset_of_POW': ∀A.oa_P (POW' A) → Ω^A ≝ λA,x.x.
coercion powerset_of_POW'.
definition powerset_of_POW': ∀A.oa_P (POW' A) → Ω^A ≝ λA,x.x.
coercion powerset_of_POW'.
| intros; split; intro;
[ intros 2; intros 2; apply (f y); exists[apply a] split; assumption;
| intros 2; change with (a ∈ q); cases f1; cases x; clear f1 x;
| intros; split; intro;
[ intros 2; intros 2; apply (f y); exists[apply a] split; assumption;
| intros 2; change with (a ∈ q); cases f1; cases x; clear f1 x;
unfold foo; intro o; intro; unfold minus_image; simplify; split; simplify; intros;
[ cases e; cases x; change with (a1 ∈ a); change in f with (a1 =_1 w);
apply (. f‡#); assumption;
unfold foo; intro o; intro; unfold minus_image; simplify; split; simplify; intros;
[ cases e; cases x; change with (a1 ∈ a); change in f with (a1 =_1 w);
apply (. f‡#); assumption;
unfold foo; intro o; intro; unfold star_image; simplify; split; simplify; intros;
[ change with (a1 ∈ a); apply f; change with (a1 =_1 a1); apply rule refl1;
| change in f1 with (a1 =_1 y); apply (. f1^-1‡#); apply f;]
unfold foo; intro o; intro; unfold star_image; simplify; split; simplify; intros;
[ change with (a1 ∈ a); apply f; change with (a1 =_1 a1); apply rule refl1;
| change in f1 with (a1 =_1 y); apply (. f1^-1‡#); apply f;]
[4: apply mem; |6: apply Hletin;|1,2,3,5: skip]
lapply (#‡prop11 ?? f ?? (†e)); [6: apply Hletin; |*:skip ]]
| (split; intro; split; simplify);
[4: apply mem; |6: apply Hletin;|1,2,3,5: skip]
lapply (#‡prop11 ?? f ?? (†e)); [6: apply Hletin; |*:skip ]]
| (split; intro; split; simplify);
[ change with (∀a1.(∀x. a1 ∈ (f {(x):S}) → x ∈ a) → a1 ∈ f⎻* a);
| change with (∀a1.a1 ∈ f⎻* a → (∀x.a1 ∈ f {(x):S} → x ∈ a));
| alias symbol "and" (instance 4) = "and_morphism".
[ change with (∀a1.(∀x. a1 ∈ (f {(x):S}) → x ∈ a) → a1 ∈ f⎻* a);
| change with (∀a1.a1 ∈ f⎻* a → (∀x.a1 ∈ f {(x):S} → x ∈ a));
| alias symbol "and" (instance 4) = "and_morphism".