wepwsolem

Description: Transfer an ordering on characteristic functions by isomorphism to the power set. (Contributed by Stefan O'Rear, 18-Jan-2015)

	Ref	Expression
Hypotheses	wepwso.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in A ((z \in y \land \neg z \in x) \land \forall w \in A (w R z \to (w \in x \leftrightarrow w \in y)))\}$
	wepwso.u	$⊢ U = \{⟨x, y⟩ \| \exists z \in A (x (z) E y (z) \land \forall w \in A (w R z \to x (w) = y (w)))\}$
	wepwso.f	$⊢ F = (a \in ({2_{𝑜}}^{A}) ⟼ a^{-1} [\{1_{𝑜}\}])$
Assertion	wepwsolem	$⊢ A \in V \to F {Isom}_{U, T} ({2_{𝑜}}^{A}, 𝒫 A)$

Proof

Step	Hyp	Ref	Expression
1		wepwso.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in A ((z \in y \land \neg z \in x) \land \forall w \in A (w R z \to (w \in x \leftrightarrow w \in y)))\}$
2		wepwso.u	$⊢ U = \{⟨x, y⟩ \| \exists z \in A (x (z) E y (z) \land \forall w \in A (w R z \to x (w) = y (w)))\}$
3		wepwso.f	$⊢ F = (a \in ({2_{𝑜}}^{A}) ⟼ a^{-1} [\{1_{𝑜}\}])$
4	3	pw2f1o2	$⊢ A \in V \to F : {2_{𝑜}}^{A} \underset{1-1 onto}{⟶} 𝒫 A$
5		fvex	$⊢ c (z) \in V$
6	5	epeli	$⊢ b (z) E c (z) \leftrightarrow b (z) \in c (z)$
7		elmapi	$⊢ b \in ({2_{𝑜}}^{A}) \to b : A ⟶ 2_{𝑜}$
8	7	ad2antrl	$⊢ (A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \to b : A ⟶ 2_{𝑜}$
9	8	ffvelrnda	$⊢ ((A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \land z \in A) \to b (z) \in 2_{𝑜}$
10		elmapi	$⊢ c \in ({2_{𝑜}}^{A}) \to c : A ⟶ 2_{𝑜}$
11	10	ad2antll	$⊢ (A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \to c : A ⟶ 2_{𝑜}$
12	11	ffvelrnda	$⊢ ((A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \land z \in A) \to c (z) \in 2_{𝑜}$
13		n0i	$⊢ b (z) \in c (z) \to \neg c (z) = \emptyset$
14	13	adantl	$⊢ ((b (z) \in 2_{𝑜} \land c (z) \in 2_{𝑜}) \land b (z) \in c (z)) \to \neg c (z) = \emptyset$
15		elpri	$⊢ c (z) \in \{\emptyset, 1_{𝑜}\} \to (c (z) = \emptyset \lor c (z) = 1_{𝑜})$
16		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
17	15 16	eleq2s	$⊢ c (z) \in 2_{𝑜} \to (c (z) = \emptyset \lor c (z) = 1_{𝑜})$
18	17	ad2antlr	$⊢ ((b (z) \in 2_{𝑜} \land c (z) \in 2_{𝑜}) \land b (z) \in c (z)) \to (c (z) = \emptyset \lor c (z) = 1_{𝑜})$
19		orel1	$⊢ \neg c (z) = \emptyset \to ((c (z) = \emptyset \lor c (z) = 1_{𝑜}) \to c (z) = 1_{𝑜})$
20	14 18 19	sylc	$⊢ ((b (z) \in 2_{𝑜} \land c (z) \in 2_{𝑜}) \land b (z) \in c (z)) \to c (z) = 1_{𝑜}$
21		1on	$⊢ 1_{𝑜} \in On$
22	21	onirri	$⊢ \neg 1_{𝑜} \in 1_{𝑜}$
23		eleq12	$⊢ (b (z) = 1_{𝑜} \land c (z) = 1_{𝑜}) \to (b (z) \in c (z) \leftrightarrow 1_{𝑜} \in 1_{𝑜})$
24	23	biimpd	$⊢ (b (z) = 1_{𝑜} \land c (z) = 1_{𝑜}) \to (b (z) \in c (z) \to 1_{𝑜} \in 1_{𝑜})$
25	24	expcom	$⊢ c (z) = 1_{𝑜} \to (b (z) = 1_{𝑜} \to (b (z) \in c (z) \to 1_{𝑜} \in 1_{𝑜}))$
26	25	com3r	$⊢ b (z) \in c (z) \to (c (z) = 1_{𝑜} \to (b (z) = 1_{𝑜} \to 1_{𝑜} \in 1_{𝑜}))$
27	26	imp	$⊢ (b (z) \in c (z) \land c (z) = 1_{𝑜}) \to (b (z) = 1_{𝑜} \to 1_{𝑜} \in 1_{𝑜})$
28	27	adantll	$⊢ (((b (z) \in 2_{𝑜} \land c (z) \in 2_{𝑜}) \land b (z) \in c (z)) \land c (z) = 1_{𝑜}) \to (b (z) = 1_{𝑜} \to 1_{𝑜} \in 1_{𝑜})$
29	22 28	mtoi	$⊢ (((b (z) \in 2_{𝑜} \land c (z) \in 2_{𝑜}) \land b (z) \in c (z)) \land c (z) = 1_{𝑜}) \to \neg b (z) = 1_{𝑜}$
30	20 29	mpdan	$⊢ ((b (z) \in 2_{𝑜} \land c (z) \in 2_{𝑜}) \land b (z) \in c (z)) \to \neg b (z) = 1_{𝑜}$
31	20 30	jca	$⊢ ((b (z) \in 2_{𝑜} \land c (z) \in 2_{𝑜}) \land b (z) \in c (z)) \to (c (z) = 1_{𝑜} \land \neg b (z) = 1_{𝑜})$
32		elpri	$⊢ b (z) \in \{\emptyset, 1_{𝑜}\} \to (b (z) = \emptyset \lor b (z) = 1_{𝑜})$
33	32 16	eleq2s	$⊢ b (z) \in 2_{𝑜} \to (b (z) = \emptyset \lor b (z) = 1_{𝑜})$
34	33	adantr	$⊢ (b (z) \in 2_{𝑜} \land c (z) \in 2_{𝑜}) \to (b (z) = \emptyset \lor b (z) = 1_{𝑜})$
35		orel2	$⊢ \neg b (z) = 1_{𝑜} \to ((b (z) = \emptyset \lor b (z) = 1_{𝑜}) \to b (z) = \emptyset)$
36	34 35	mpan9	$⊢ ((b (z) \in 2_{𝑜} \land c (z) \in 2_{𝑜}) \land \neg b (z) = 1_{𝑜}) \to b (z) = \emptyset$
37	36	adantrl	$⊢ ((b (z) \in 2_{𝑜} \land c (z) \in 2_{𝑜}) \land (c (z) = 1_{𝑜} \land \neg b (z) = 1_{𝑜})) \to b (z) = \emptyset$
38		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
39	37 38	eqeltrdi	$⊢ ((b (z) \in 2_{𝑜} \land c (z) \in 2_{𝑜}) \land (c (z) = 1_{𝑜} \land \neg b (z) = 1_{𝑜})) \to b (z) \in 1_{𝑜}$
40		simprl	$⊢ ((b (z) \in 2_{𝑜} \land c (z) \in 2_{𝑜}) \land (c (z) = 1_{𝑜} \land \neg b (z) = 1_{𝑜})) \to c (z) = 1_{𝑜}$
41	39 40	eleqtrrd	$⊢ ((b (z) \in 2_{𝑜} \land c (z) \in 2_{𝑜}) \land (c (z) = 1_{𝑜} \land \neg b (z) = 1_{𝑜})) \to b (z) \in c (z)$
42	31 41	impbida	$⊢ (b (z) \in 2_{𝑜} \land c (z) \in 2_{𝑜}) \to (b (z) \in c (z) \leftrightarrow (c (z) = 1_{𝑜} \land \neg b (z) = 1_{𝑜}))$
43	9 12 42	syl2anc	$⊢ ((A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \land z \in A) \to (b (z) \in c (z) \leftrightarrow (c (z) = 1_{𝑜} \land \neg b (z) = 1_{𝑜}))$
44		simplrr	$⊢ ((A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \land z \in A) \to c \in ({2_{𝑜}}^{A})$
45	3	pw2f1o2val2	$⊢ (c \in ({2_{𝑜}}^{A}) \land z \in A) \to (z \in F (c) \leftrightarrow c (z) = 1_{𝑜})$
46	44 45	sylancom	$⊢ ((A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \land z \in A) \to (z \in F (c) \leftrightarrow c (z) = 1_{𝑜})$
47		simplrl	$⊢ ((A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \land z \in A) \to b \in ({2_{𝑜}}^{A})$
48	3	pw2f1o2val2	$⊢ (b \in ({2_{𝑜}}^{A}) \land z \in A) \to (z \in F (b) \leftrightarrow b (z) = 1_{𝑜})$
49	47 48	sylancom	$⊢ ((A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \land z \in A) \to (z \in F (b) \leftrightarrow b (z) = 1_{𝑜})$
50	49	notbid	$⊢ ((A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \land z \in A) \to (\neg z \in F (b) \leftrightarrow \neg b (z) = 1_{𝑜})$
51	46 50	anbi12d	$⊢ ((A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \land z \in A) \to ((z \in F (c) \land \neg z \in F (b)) \leftrightarrow (c (z) = 1_{𝑜} \land \neg b (z) = 1_{𝑜}))$
52	43 51	bitr4d	$⊢ ((A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \land z \in A) \to (b (z) \in c (z) \leftrightarrow (z \in F (c) \land \neg z \in F (b)))$
53	6 52	syl5bb	$⊢ ((A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \land z \in A) \to (b (z) E c (z) \leftrightarrow (z \in F (c) \land \neg z \in F (b)))$
54	8	ffvelrnda	$⊢ ((A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \land w \in A) \to b (w) \in 2_{𝑜}$
55	11	ffvelrnda	$⊢ ((A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \land w \in A) \to c (w) \in 2_{𝑜}$
56		eqeq1	$⊢ b (w) = c (w) \to (b (w) = 1_{𝑜} \leftrightarrow c (w) = 1_{𝑜})$
57		simplr	$⊢ (((b (w) \in 2_{𝑜} \land c (w) \in 2_{𝑜}) \land b (w) = \emptyset) \land (b (w) = 1_{𝑜} \leftrightarrow c (w) = 1_{𝑜})) \to b (w) = \emptyset$
58		1n0	$⊢ 1_{𝑜} \neq \emptyset$
59	58	nesymi	$⊢ \neg \emptyset = 1_{𝑜}$
60		eqeq1	$⊢ b (w) = \emptyset \to (b (w) = 1_{𝑜} \leftrightarrow \emptyset = 1_{𝑜})$
61	59 60	mtbiri	$⊢ b (w) = \emptyset \to \neg b (w) = 1_{𝑜}$
62	61	ad2antlr	$⊢ (((b (w) \in 2_{𝑜} \land c (w) \in 2_{𝑜}) \land b (w) = \emptyset) \land (b (w) = 1_{𝑜} \leftrightarrow c (w) = 1_{𝑜})) \to \neg b (w) = 1_{𝑜}$
63		simpr	$⊢ (((b (w) \in 2_{𝑜} \land c (w) \in 2_{𝑜}) \land b (w) = \emptyset) \land (b (w) = 1_{𝑜} \leftrightarrow c (w) = 1_{𝑜})) \to (b (w) = 1_{𝑜} \leftrightarrow c (w) = 1_{𝑜})$
64	62 63	mtbid	$⊢ (((b (w) \in 2_{𝑜} \land c (w) \in 2_{𝑜}) \land b (w) = \emptyset) \land (b (w) = 1_{𝑜} \leftrightarrow c (w) = 1_{𝑜})) \to \neg c (w) = 1_{𝑜}$
65		elpri	$⊢ c (w) \in \{\emptyset, 1_{𝑜}\} \to (c (w) = \emptyset \lor c (w) = 1_{𝑜})$
66	65 16	eleq2s	$⊢ c (w) \in 2_{𝑜} \to (c (w) = \emptyset \lor c (w) = 1_{𝑜})$
67	66	ad3antlr	$⊢ (((b (w) \in 2_{𝑜} \land c (w) \in 2_{𝑜}) \land b (w) = \emptyset) \land (b (w) = 1_{𝑜} \leftrightarrow c (w) = 1_{𝑜})) \to (c (w) = \emptyset \lor c (w) = 1_{𝑜})$
68		orel2	$⊢ \neg c (w) = 1_{𝑜} \to ((c (w) = \emptyset \lor c (w) = 1_{𝑜}) \to c (w) = \emptyset)$
69	64 67 68	sylc	$⊢ (((b (w) \in 2_{𝑜} \land c (w) \in 2_{𝑜}) \land b (w) = \emptyset) \land (b (w) = 1_{𝑜} \leftrightarrow c (w) = 1_{𝑜})) \to c (w) = \emptyset$
70	57 69	eqtr4d	$⊢ (((b (w) \in 2_{𝑜} \land c (w) \in 2_{𝑜}) \land b (w) = \emptyset) \land (b (w) = 1_{𝑜} \leftrightarrow c (w) = 1_{𝑜})) \to b (w) = c (w)$
71	70	ex	$⊢ ((b (w) \in 2_{𝑜} \land c (w) \in 2_{𝑜}) \land b (w) = \emptyset) \to ((b (w) = 1_{𝑜} \leftrightarrow c (w) = 1_{𝑜}) \to b (w) = c (w))$
72		simplr	$⊢ (((b (w) \in 2_{𝑜} \land c (w) \in 2_{𝑜}) \land b (w) = 1_{𝑜}) \land (b (w) = 1_{𝑜} \leftrightarrow c (w) = 1_{𝑜})) \to b (w) = 1_{𝑜}$
73		simpr	$⊢ (((b (w) \in 2_{𝑜} \land c (w) \in 2_{𝑜}) \land b (w) = 1_{𝑜}) \land (b (w) = 1_{𝑜} \leftrightarrow c (w) = 1_{𝑜})) \to (b (w) = 1_{𝑜} \leftrightarrow c (w) = 1_{𝑜})$
74	72 73	mpbid	$⊢ (((b (w) \in 2_{𝑜} \land c (w) \in 2_{𝑜}) \land b (w) = 1_{𝑜}) \land (b (w) = 1_{𝑜} \leftrightarrow c (w) = 1_{𝑜})) \to c (w) = 1_{𝑜}$
75	72 74	eqtr4d	$⊢ (((b (w) \in 2_{𝑜} \land c (w) \in 2_{𝑜}) \land b (w) = 1_{𝑜}) \land (b (w) = 1_{𝑜} \leftrightarrow c (w) = 1_{𝑜})) \to b (w) = c (w)$
76	75	ex	$⊢ ((b (w) \in 2_{𝑜} \land c (w) \in 2_{𝑜}) \land b (w) = 1_{𝑜}) \to ((b (w) = 1_{𝑜} \leftrightarrow c (w) = 1_{𝑜}) \to b (w) = c (w))$
77		elpri	$⊢ b (w) \in \{\emptyset, 1_{𝑜}\} \to (b (w) = \emptyset \lor b (w) = 1_{𝑜})$
78	77 16	eleq2s	$⊢ b (w) \in 2_{𝑜} \to (b (w) = \emptyset \lor b (w) = 1_{𝑜})$
79	78	adantr	$⊢ (b (w) \in 2_{𝑜} \land c (w) \in 2_{𝑜}) \to (b (w) = \emptyset \lor b (w) = 1_{𝑜})$
80	71 76 79	mpjaodan	$⊢ (b (w) \in 2_{𝑜} \land c (w) \in 2_{𝑜}) \to ((b (w) = 1_{𝑜} \leftrightarrow c (w) = 1_{𝑜}) \to b (w) = c (w))$
81	56 80	impbid2	$⊢ (b (w) \in 2_{𝑜} \land c (w) \in 2_{𝑜}) \to (b (w) = c (w) \leftrightarrow (b (w) = 1_{𝑜} \leftrightarrow c (w) = 1_{𝑜}))$
82	54 55 81	syl2anc	$⊢ ((A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \land w \in A) \to (b (w) = c (w) \leftrightarrow (b (w) = 1_{𝑜} \leftrightarrow c (w) = 1_{𝑜}))$
83		simplrl	$⊢ ((A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \land w \in A) \to b \in ({2_{𝑜}}^{A})$
84	3	pw2f1o2val2	$⊢ (b \in ({2_{𝑜}}^{A}) \land w \in A) \to (w \in F (b) \leftrightarrow b (w) = 1_{𝑜})$
85	83 84	sylancom	$⊢ ((A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \land w \in A) \to (w \in F (b) \leftrightarrow b (w) = 1_{𝑜})$
86		simplrr	$⊢ ((A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \land w \in A) \to c \in ({2_{𝑜}}^{A})$
87	3	pw2f1o2val2	$⊢ (c \in ({2_{𝑜}}^{A}) \land w \in A) \to (w \in F (c) \leftrightarrow c (w) = 1_{𝑜})$
88	86 87	sylancom	$⊢ ((A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \land w \in A) \to (w \in F (c) \leftrightarrow c (w) = 1_{𝑜})$
89	85 88	bibi12d	$⊢ ((A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \land w \in A) \to ((w \in F (b) \leftrightarrow w \in F (c)) \leftrightarrow (b (w) = 1_{𝑜} \leftrightarrow c (w) = 1_{𝑜}))$
90	82 89	bitr4d	$⊢ ((A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \land w \in A) \to (b (w) = c (w) \leftrightarrow (w \in F (b) \leftrightarrow w \in F (c)))$
91	90	imbi2d	$⊢ ((A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \land w \in A) \to ((w R z \to b (w) = c (w)) \leftrightarrow (w R z \to (w \in F (b) \leftrightarrow w \in F (c))))$
92	91	ralbidva	$⊢ (A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \to (\forall w \in A (w R z \to b (w) = c (w)) \leftrightarrow \forall w \in A (w R z \to (w \in F (b) \leftrightarrow w \in F (c))))$
93	92	adantr	$⊢ ((A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \land z \in A) \to (\forall w \in A (w R z \to b (w) = c (w)) \leftrightarrow \forall w \in A (w R z \to (w \in F (b) \leftrightarrow w \in F (c))))$
94	53 93	anbi12d	$⊢ ((A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \land z \in A) \to ((b (z) E c (z) \land \forall w \in A (w R z \to b (w) = c (w))) \leftrightarrow ((z \in F (c) \land \neg z \in F (b)) \land \forall w \in A (w R z \to (w \in F (b) \leftrightarrow w \in F (c)))))$
95	94	rexbidva	$⊢ (A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \to (\exists z \in A (b (z) E c (z) \land \forall w \in A (w R z \to b (w) = c (w))) \leftrightarrow \exists z \in A ((z \in F (c) \land \neg z \in F (b)) \land \forall w \in A (w R z \to (w \in F (b) \leftrightarrow w \in F (c)))))$
96		vex	$⊢ b \in V$
97		vex	$⊢ c \in V$
98		fveq1	$⊢ x = b \to x (z) = b (z)$
99		fveq1	$⊢ y = c \to y (z) = c (z)$
100	98 99	breqan12d	$⊢ (x = b \land y = c) \to (x (z) E y (z) \leftrightarrow b (z) E c (z))$
101		fveq1	$⊢ x = b \to x (w) = b (w)$
102		fveq1	$⊢ y = c \to y (w) = c (w)$
103	101 102	eqeqan12d	$⊢ (x = b \land y = c) \to (x (w) = y (w) \leftrightarrow b (w) = c (w))$
104	103	imbi2d	$⊢ (x = b \land y = c) \to ((w R z \to x (w) = y (w)) \leftrightarrow (w R z \to b (w) = c (w)))$
105	104	ralbidv	$⊢ (x = b \land y = c) \to (\forall w \in A (w R z \to x (w) = y (w)) \leftrightarrow \forall w \in A (w R z \to b (w) = c (w)))$
106	100 105	anbi12d	$⊢ (x = b \land y = c) \to ((x (z) E y (z) \land \forall w \in A (w R z \to x (w) = y (w))) \leftrightarrow (b (z) E c (z) \land \forall w \in A (w R z \to b (w) = c (w))))$
107	106	rexbidv	$⊢ (x = b \land y = c) \to (\exists z \in A (x (z) E y (z) \land \forall w \in A (w R z \to x (w) = y (w))) \leftrightarrow \exists z \in A (b (z) E c (z) \land \forall w \in A (w R z \to b (w) = c (w))))$
108	96 97 107 2	braba	$⊢ b U c \leftrightarrow \exists z \in A (b (z) E c (z) \land \forall w \in A (w R z \to b (w) = c (w)))$
109		fvex	$⊢ F (b) \in V$
110		fvex	$⊢ F (c) \in V$
111		eleq2	$⊢ y = F (c) \to (z \in y \leftrightarrow z \in F (c))$
112		eleq2	$⊢ x = F (b) \to (z \in x \leftrightarrow z \in F (b))$
113	112	notbid	$⊢ x = F (b) \to (\neg z \in x \leftrightarrow \neg z \in F (b))$
114	111 113	bi2anan9r	$⊢ (x = F (b) \land y = F (c)) \to ((z \in y \land \neg z \in x) \leftrightarrow (z \in F (c) \land \neg z \in F (b)))$
115		eleq2	$⊢ x = F (b) \to (w \in x \leftrightarrow w \in F (b))$
116		eleq2	$⊢ y = F (c) \to (w \in y \leftrightarrow w \in F (c))$
117	115 116	bi2bian9	$⊢ (x = F (b) \land y = F (c)) \to ((w \in x \leftrightarrow w \in y) \leftrightarrow (w \in F (b) \leftrightarrow w \in F (c)))$
118	117	imbi2d	$⊢ (x = F (b) \land y = F (c)) \to ((w R z \to (w \in x \leftrightarrow w \in y)) \leftrightarrow (w R z \to (w \in F (b) \leftrightarrow w \in F (c))))$
119	118	ralbidv	$⊢ (x = F (b) \land y = F (c)) \to (\forall w \in A (w R z \to (w \in x \leftrightarrow w \in y)) \leftrightarrow \forall w \in A (w R z \to (w \in F (b) \leftrightarrow w \in F (c))))$
120	114 119	anbi12d	$⊢ (x = F (b) \land y = F (c)) \to (((z \in y \land \neg z \in x) \land \forall w \in A (w R z \to (w \in x \leftrightarrow w \in y))) \leftrightarrow ((z \in F (c) \land \neg z \in F (b)) \land \forall w \in A (w R z \to (w \in F (b) \leftrightarrow w \in F (c)))))$
121	120	rexbidv	$⊢ (x = F (b) \land y = F (c)) \to (\exists z \in A ((z \in y \land \neg z \in x) \land \forall w \in A (w R z \to (w \in x \leftrightarrow w \in y))) \leftrightarrow \exists z \in A ((z \in F (c) \land \neg z \in F (b)) \land \forall w \in A (w R z \to (w \in F (b) \leftrightarrow w \in F (c)))))$
122	109 110 121 1	braba	$⊢ F (b) T F (c) \leftrightarrow \exists z \in A ((z \in F (c) \land \neg z \in F (b)) \land \forall w \in A (w R z \to (w \in F (b) \leftrightarrow w \in F (c))))$
123	95 108 122	3bitr4g	$⊢ (A \in V \land (b \in ({2_{𝑜}}^{A}) \land c \in ({2_{𝑜}}^{A}))) \to (b U c \leftrightarrow F (b) T F (c))$
124	123	ralrimivva	$⊢ A \in V \to \forall b \in ({2_{𝑜}}^{A}) \forall c \in ({2_{𝑜}}^{A}) (b U c \leftrightarrow F (b) T F (c))$
125		df-isom	$⊢ F {Isom}_{U, T} ({2_{𝑜}}^{A}, 𝒫 A) \leftrightarrow (F : {2_{𝑜}}^{A} \underset{1-1 onto}{⟶} 𝒫 A \land \forall b \in ({2_{𝑜}}^{A}) \forall c \in ({2_{𝑜}}^{A}) (b U c \leftrightarrow F (b) T F (c)))$
126	4 124 125	sylanbrc	$⊢ A \in V \to F {Isom}_{U, T} ({2_{𝑜}}^{A}, 𝒫 A)$

Metamath Proof Explorer

Theorem wepwsolem

Proof