canthwelem

	Ref	Expression
Hypotheses	canthwe.1	$⊢ O = \{⟨x, r⟩ \| (x \subseteq A \land r \subseteq x \times x \land r We x)\}$
	canthwe.2	$⊢ W = \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y))\}$
	canthwe.3	$⊢ B = ⋃ dom W$
	canthwe.4	$⊢ C = {W (B)}^{-1} [\{B F W (B)\}]$
Assertion	canthwelem	$⊢ A \in V \to \neg F : O \underset{1-1}{⟶} A$

Proof

Step	Hyp	Ref	Expression
1		canthwe.1	$⊢ O = \{⟨x, r⟩ \| (x \subseteq A \land r \subseteq x \times x \land r We x)\}$
2		canthwe.2	$⊢ W = \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y))\}$
3		canthwe.3	$⊢ B = ⋃ dom W$
4		canthwe.4	$⊢ C = {W (B)}^{-1} [\{B F W (B)\}]$
5		eqid	$⊢ B = B$
6		eqid	$⊢ W (B) = W (B)$
7	5 6	pm3.2i	$⊢ (B = B \land W (B) = W (B))$
8		simpl	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to A \in V$
9		df-ov	$⊢ x F r = F (⟨x, r⟩)$
10		f1f	$⊢ F : O \underset{1-1}{⟶} A \to F : O ⟶ A$
11	10	ad2antlr	$⊢ ((A \in V \land F : O \underset{1-1}{⟶} A) \land (x \subseteq A \land r \subseteq x \times x \land r We x)) \to F : O ⟶ A$
12		simpr	$⊢ ((A \in V \land F : O \underset{1-1}{⟶} A) \land (x \subseteq A \land r \subseteq x \times x \land r We x)) \to (x \subseteq A \land r \subseteq x \times x \land r We x)$
13		opabidw	$⊢ ⟨x, r⟩ \in \{⟨x, r⟩ \| (x \subseteq A \land r \subseteq x \times x \land r We x)\} \leftrightarrow (x \subseteq A \land r \subseteq x \times x \land r We x)$
14	12 13	sylibr	$⊢ ((A \in V \land F : O \underset{1-1}{⟶} A) \land (x \subseteq A \land r \subseteq x \times x \land r We x)) \to ⟨x, r⟩ \in \{⟨x, r⟩ \| (x \subseteq A \land r \subseteq x \times x \land r We x)\}$
15	14 1	eleqtrrdi	$⊢ ((A \in V \land F : O \underset{1-1}{⟶} A) \land (x \subseteq A \land r \subseteq x \times x \land r We x)) \to ⟨x, r⟩ \in O$
16	11 15	ffvelcdmd	$⊢ ((A \in V \land F : O \underset{1-1}{⟶} A) \land (x \subseteq A \land r \subseteq x \times x \land r We x)) \to F (⟨x, r⟩) \in A$
17	9 16	eqeltrid	$⊢ ((A \in V \land F : O \underset{1-1}{⟶} A) \land (x \subseteq A \land r \subseteq x \times x \land r We x)) \to x F r \in A$
18	2 8 17 3	fpwwe2	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to ((B W W (B) \land B F W (B) \in B) \leftrightarrow (B = B \land W (B) = W (B)))$
19	7 18	mpbiri	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to (B W W (B) \land B F W (B) \in B)$
20	19	simprd	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to B F W (B) \in B$
21	4 4	xpeq12i	$⊢ C \times C = {W (B)}^{-1} [\{B F W (B)\}] \times {W (B)}^{-1} [\{B F W (B)\}]$
22	21	ineq2i	$⊢ W (B) \cap (C \times C) = W (B) \cap ({W (B)}^{-1} [\{B F W (B)\}] \times {W (B)}^{-1} [\{B F W (B)\}])$
23	4 22	oveq12i	$⊢ C F (W (B) \cap (C \times C)) = {W (B)}^{-1} [\{B F W (B)\}] F (W (B) \cap ({W (B)}^{-1} [\{B F W (B)\}] \times {W (B)}^{-1} [\{B F W (B)\}]))$
24	19	simpld	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to B W W (B)$
25	2 8 24	fpwwe2lem3	$⊢ ((A \in V \land F : O \underset{1-1}{⟶} A) \land B F W (B) \in B) \to {W (B)}^{-1} [\{B F W (B)\}] F (W (B) \cap ({W (B)}^{-1} [\{B F W (B)\}] \times {W (B)}^{-1} [\{B F W (B)\}])) = B F W (B)$
26	20 25	mpdan	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to {W (B)}^{-1} [\{B F W (B)\}] F (W (B) \cap ({W (B)}^{-1} [\{B F W (B)\}] \times {W (B)}^{-1} [\{B F W (B)\}])) = B F W (B)$
27	23 26	eqtrid	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to C F (W (B) \cap (C \times C)) = B F W (B)$
28		df-ov	$⊢ C F (W (B) \cap (C \times C)) = F (⟨C, W (B) \cap (C \times C)⟩)$
29		df-ov	$⊢ B F W (B) = F (⟨B, W (B)⟩)$
30	27 28 29	3eqtr3g	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to F (⟨C, W (B) \cap (C \times C)⟩) = F (⟨B, W (B)⟩)$
31		simpr	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to F : O \underset{1-1}{⟶} A$
32		cnvimass	$⊢ {W (B)}^{-1} [\{B F W (B)\}] \subseteq dom W (B)$
33	2 8	fpwwe2lem2	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to (B W W (B) \leftrightarrow ((B \subseteq A \land W (B) \subseteq B \times B) \land (W (B) We B \land \forall y \in B \underset{˙}{[} {W (B)}^{-1} [\{y\}] / u \underset{˙}{]} u F (W (B) \cap (u \times u)) = y)))$
34	24 33	mpbid	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to ((B \subseteq A \land W (B) \subseteq B \times B) \land (W (B) We B \land \forall y \in B \underset{˙}{[} {W (B)}^{-1} [\{y\}] / u \underset{˙}{]} u F (W (B) \cap (u \times u)) = y))$
35	34	simpld	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to (B \subseteq A \land W (B) \subseteq B \times B)$
36	35	simprd	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to W (B) \subseteq B \times B$
37		dmss	$⊢ W (B) \subseteq B \times B \to dom W (B) \subseteq dom (B \times B)$
38	36 37	syl	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to dom W (B) \subseteq dom (B \times B)$
39		dmxpss	$⊢ dom (B \times B) \subseteq B$
40	38 39	sstrdi	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to dom W (B) \subseteq B$
41	32 40	sstrid	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to {W (B)}^{-1} [\{B F W (B)\}] \subseteq B$
42	4 41	eqsstrid	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to C \subseteq B$
43	35	simpld	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to B \subseteq A$
44	42 43	sstrd	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to C \subseteq A$
45		inss2	$⊢ W (B) \cap (C \times C) \subseteq C \times C$
46	45	a1i	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to W (B) \cap (C \times C) \subseteq C \times C$
47	34	simprd	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to (W (B) We B \land \forall y \in B \underset{˙}{[} {W (B)}^{-1} [\{y\}] / u \underset{˙}{]} u F (W (B) \cap (u \times u)) = y)$
48	47	simpld	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to W (B) We B$
49		wess	$⊢ C \subseteq B \to (W (B) We B \to W (B) We C)$
50	42 48 49	sylc	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to W (B) We C$
51		weinxp	$⊢ W (B) We C \leftrightarrow (W (B) \cap (C \times C)) We C$
52	50 51	sylib	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to (W (B) \cap (C \times C)) We C$
53		fvex	$⊢ W (B) \in V$
54	53	cnvex	$⊢ {W (B)}^{-1} \in V$
55	54	imaex	$⊢ {W (B)}^{-1} [\{B F W (B)\}] \in V$
56	4 55	eqeltri	$⊢ C \in V$
57	53	inex1	$⊢ W (B) \cap (C \times C) \in V$
58		simpl	$⊢ (x = C \land r = W (B) \cap (C \times C)) \to x = C$
59	58	sseq1d	$⊢ (x = C \land r = W (B) \cap (C \times C)) \to (x \subseteq A \leftrightarrow C \subseteq A)$
60		simpr	$⊢ (x = C \land r = W (B) \cap (C \times C)) \to r = W (B) \cap (C \times C)$
61	58	sqxpeqd	$⊢ (x = C \land r = W (B) \cap (C \times C)) \to x \times x = C \times C$
62	60 61	sseq12d	$⊢ (x = C \land r = W (B) \cap (C \times C)) \to (r \subseteq x \times x \leftrightarrow W (B) \cap (C \times C) \subseteq C \times C)$
63		weeq2	$⊢ x = C \to (r We x \leftrightarrow r We C)$
64		weeq1	$⊢ r = W (B) \cap (C \times C) \to (r We C \leftrightarrow (W (B) \cap (C \times C)) We C)$
65	63 64	sylan9bb	$⊢ (x = C \land r = W (B) \cap (C \times C)) \to (r We x \leftrightarrow (W (B) \cap (C \times C)) We C)$
66	59 62 65	3anbi123d	$⊢ (x = C \land r = W (B) \cap (C \times C)) \to ((x \subseteq A \land r \subseteq x \times x \land r We x) \leftrightarrow (C \subseteq A \land W (B) \cap (C \times C) \subseteq C \times C \land (W (B) \cap (C \times C)) We C))$
67	56 57 66	opelopaba	$⊢ ⟨C, W (B) \cap (C \times C)⟩ \in \{⟨x, r⟩ \| (x \subseteq A \land r \subseteq x \times x \land r We x)\} \leftrightarrow (C \subseteq A \land W (B) \cap (C \times C) \subseteq C \times C \land (W (B) \cap (C \times C)) We C)$
68	44 46 52 67	syl3anbrc	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to ⟨C, W (B) \cap (C \times C)⟩ \in \{⟨x, r⟩ \| (x \subseteq A \land r \subseteq x \times x \land r We x)\}$
69	68 1	eleqtrrdi	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to ⟨C, W (B) \cap (C \times C)⟩ \in O$
70	8 43	ssexd	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to B \in V$
71	53	a1i	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to W (B) \in V$
72		simpl	$⊢ (x = B \land r = W (B)) \to x = B$
73	72	sseq1d	$⊢ (x = B \land r = W (B)) \to (x \subseteq A \leftrightarrow B \subseteq A)$
74		simpr	$⊢ (x = B \land r = W (B)) \to r = W (B)$
75	72	sqxpeqd	$⊢ (x = B \land r = W (B)) \to x \times x = B \times B$
76	74 75	sseq12d	$⊢ (x = B \land r = W (B)) \to (r \subseteq x \times x \leftrightarrow W (B) \subseteq B \times B)$
77		weeq2	$⊢ x = B \to (r We x \leftrightarrow r We B)$
78		weeq1	$⊢ r = W (B) \to (r We B \leftrightarrow W (B) We B)$
79	77 78	sylan9bb	$⊢ (x = B \land r = W (B)) \to (r We x \leftrightarrow W (B) We B)$
80	73 76 79	3anbi123d	$⊢ (x = B \land r = W (B)) \to ((x \subseteq A \land r \subseteq x \times x \land r We x) \leftrightarrow (B \subseteq A \land W (B) \subseteq B \times B \land W (B) We B))$
81	80	opelopabga	$⊢ (B \in V \land W (B) \in V) \to (⟨B, W (B)⟩ \in \{⟨x, r⟩ \| (x \subseteq A \land r \subseteq x \times x \land r We x)\} \leftrightarrow (B \subseteq A \land W (B) \subseteq B \times B \land W (B) We B))$
82	70 71 81	syl2anc	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to (⟨B, W (B)⟩ \in \{⟨x, r⟩ \| (x \subseteq A \land r \subseteq x \times x \land r We x)\} \leftrightarrow (B \subseteq A \land W (B) \subseteq B \times B \land W (B) We B))$
83	43 36 48 82	mpbir3and	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to ⟨B, W (B)⟩ \in \{⟨x, r⟩ \| (x \subseteq A \land r \subseteq x \times x \land r We x)\}$
84	83 1	eleqtrrdi	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to ⟨B, W (B)⟩ \in O$
85		f1fveq	$⊢ (F : O \underset{1-1}{⟶} A \land (⟨C, W (B) \cap (C \times C)⟩ \in O \land ⟨B, W (B)⟩ \in O)) \to (F (⟨C, W (B) \cap (C \times C)⟩) = F (⟨B, W (B)⟩) \leftrightarrow ⟨C, W (B) \cap (C \times C)⟩ = ⟨B, W (B)⟩)$
86	31 69 84 85	syl12anc	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to (F (⟨C, W (B) \cap (C \times C)⟩) = F (⟨B, W (B)⟩) \leftrightarrow ⟨C, W (B) \cap (C \times C)⟩ = ⟨B, W (B)⟩)$
87	30 86	mpbid	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to ⟨C, W (B) \cap (C \times C)⟩ = ⟨B, W (B)⟩$
88	56 57	opth1	$⊢ ⟨C, W (B) \cap (C \times C)⟩ = ⟨B, W (B)⟩ \to C = B$
89	87 88	syl	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to C = B$
90	20 89	eleqtrrd	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to B F W (B) \in C$
91	90 4	eleqtrdi	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to B F W (B) \in {W (B)}^{-1} [\{B F W (B)\}]$
92		ovex	$⊢ B F W (B) \in V$
93	92	eliniseg	$⊢ B F W (B) \in B \to (B F W (B) \in {W (B)}^{-1} [\{B F W (B)\}] \leftrightarrow (B F W (B)) W (B) (B F W (B)))$
94	20 93	syl	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to (B F W (B) \in {W (B)}^{-1} [\{B F W (B)\}] \leftrightarrow (B F W (B)) W (B) (B F W (B)))$
95	91 94	mpbid	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to (B F W (B)) W (B) (B F W (B))$
96		weso	$⊢ W (B) We B \to W (B) Or B$
97	48 96	syl	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to W (B) Or B$
98		sonr	$⊢ (W (B) Or B \land B F W (B) \in B) \to \neg (B F W (B)) W (B) (B F W (B))$
99	97 20 98	syl2anc	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to \neg (B F W (B)) W (B) (B F W (B))$
100	95 99	pm2.65da	$⊢ A \in V \to \neg F : O \underset{1-1}{⟶} A$

Metamath Proof Explorer

Theorem canthwelem

Proof