Theorem membpartlem19

Description: Together with disjlem19 , this is former prtlem19 . (Contributed by Rodolfo Medina, 15-Oct-2010) (Revised by Mario Carneiro, 12-Aug-2015) (Revised by Peter Mazsa, 21-Oct-2021)

	Ref	Expression
Assertion	membpartlem19	Could not format assertion : No typesetting found for |- ( B e. V -> ( MembPart A -> ( ( u e. A /\ B e. u ) -> u = [ B ] ~ A ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dfmembpart2	Could not format ( MembPart A <-> ( ElDisj A /\ -. (/) e. A ) ) : No typesetting found for |- ( MembPart A <-> ( ElDisj A /\ -. (/) e. A ) ) with typecode |-
2		n0el2	$$⊢\neg \varnothing \in A\leftrightarrow \mathrm{dom}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A$$
3	2	biimpi	$$⊢\neg \varnothing \in A\to \mathrm{dom}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A$$
4	3	ad2antll	$$⊢\left(B\in V\wedge \left(ElDisjA\wedge \neg \varnothing \in A\right)\right)\to \mathrm{dom}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A$$
5	4	eleq2d	$$⊢\left(B\in V\wedge \left(ElDisjA\wedge \neg \varnothing \in A\right)\right)\to \left(u\in \mathrm{dom}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\leftrightarrow u\in A\right)$$
6		eldisjlem19	$$⊢B\in V\to \left(ElDisjA\to \left(\left(u\in \mathrm{dom}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\wedge B\in u\right)\to u=\left[B\right]\sim A\right)\right)$$
7	6	adantrd	$$⊢B\in V\to \left(\left(ElDisjA\wedge \neg \varnothing \in A\right)\to \left(\left(u\in \mathrm{dom}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\wedge B\in u\right)\to u=\left[B\right]\sim A\right)\right)$$
8	7	imp	$$⊢\left(B\in V\wedge \left(ElDisjA\wedge \neg \varnothing \in A\right)\right)\to \left(\left(u\in \mathrm{dom}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\wedge B\in u\right)\to u=\left[B\right]\sim A\right)$$
9	8	expd	$$⊢\left(B\in V\wedge \left(ElDisjA\wedge \neg \varnothing \in A\right)\right)\to \left(u\in \mathrm{dom}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\to \left(B\in u\to u=\left[B\right]\sim A\right)\right)$$
10	5 9	sylbird	$$⊢\left(B\in V\wedge \left(ElDisjA\wedge \neg \varnothing \in A\right)\right)\to \left(u\in A\to \left(B\in u\to u=\left[B\right]\sim A\right)\right)$$
11	1 10	sylan2b	Could not format ( ( B e. V /\ MembPart A ) -> ( u e. A -> ( B e. u -> u = [ B ] ~ A ) ) ) : No typesetting found for |- ( ( B e. V /\ MembPart A ) -> ( u e. A -> ( B e. u -> u = [ B ] ~ A ) ) ) with typecode |-
12	11	impd	Could not format ( ( B e. V /\ MembPart A ) -> ( ( u e. A /\ B e. u ) -> u = [ B ] ~ A ) ) : No typesetting found for |- ( ( B e. V /\ MembPart A ) -> ( ( u e. A /\ B e. u ) -> u = [ B ] ~ A ) ) with typecode |-
13	12	ex	Could not format ( B e. V -> ( MembPart A -> ( ( u e. A /\ B e. u ) -> u = [ B ] ~ A ) ) ) : No typesetting found for |- ( B e. V -> ( MembPart A -> ( ( u e. A /\ B e. u ) -> u = [ B ] ~ A ) ) ) with typecode |-