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		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)$
13	12	bilanri	$⊢ ((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)\}$
14	13 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$
15	11 14	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$
16	9 15	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$
17	2 8 16 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)))$
18	7 17	mpbiri	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to (B W W (B) \land B F W (B) \in B)$
19	18	simprd	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to B F W (B) \in B$
20	4 4	xpeq12i	$⊢ C \times C = {W (B)}^{-1} [\{B F W (B)\}] \times {W (B)}^{-1} [\{B F W (B)\}]$
21	20	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)\}])$
22	4 21	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)\}]))$
23	18	simpld	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to B W W (B)$
24	2 8 23	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)$
25	19 24	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)$
26	22 25	eqtrid	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to C F (W (B) \cap (C \times C)) = B F W (B)$
27		df-ov	$⊢ C F (W (B) \cap (C \times C)) = F (⟨C, W (B) \cap (C \times C)⟩)$
28		df-ov	$⊢ B F W (B) = F (⟨B, W (B)⟩)$
29	26 27 28	3eqtr3g	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to F (⟨C, W (B) \cap (C \times C)⟩) = F (⟨B, W (B)⟩)$
30		simpr	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to F : O \underset{1-1}{⟶} A$
31		cnvimass	$⊢ {W (B)}^{-1} [\{B F W (B)\}] \subseteq dom W (B)$
32	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)))$
33	23 32	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))$
34	33	simpld	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to (B \subseteq A \land W (B) \subseteq B \times B)$
35	34	simprd	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to W (B) \subseteq B \times B$
36		dmss	$⊢ W (B) \subseteq B \times B \to dom W (B) \subseteq dom (B \times B)$
37	35 36	syl	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to dom W (B) \subseteq dom (B \times B)$
38		dmxpss	$⊢ dom (B \times B) \subseteq B$
39	37 38	sstrdi	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to dom W (B) \subseteq B$
40	31 39	sstrid	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to {W (B)}^{-1} [\{B F W (B)\}] \subseteq B$
41	4 40	eqsstrid	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to C \subseteq B$
42	34	simpld	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to B \subseteq A$
43	41 42	sstrd	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to C \subseteq A$
44		inss2	$⊢ W (B) \cap (C \times C) \subseteq C \times C$
45	44	a1i	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to W (B) \cap (C \times C) \subseteq C \times C$
46	33	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)$
47	46	simpld	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to W (B) We B$
48		wess	$⊢ C \subseteq B \to (W (B) We B \to W (B) We C)$
49	41 47 48	sylc	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to W (B) We C$
50		weinxp	$⊢ W (B) We C \leftrightarrow (W (B) \cap (C \times C)) We C$
51	49 50	sylib	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to (W (B) \cap (C \times C)) We C$
52		fvex	$⊢ W (B) \in V$
53	52	cnvex	$⊢ {W (B)}^{-1} \in V$
54	53	imaex	$⊢ {W (B)}^{-1} [\{B F W (B)\}] \in V$
55	4 54	eqeltri	$⊢ C \in V$
56	52	inex1	$⊢ W (B) \cap (C \times C) \in V$
57		simpl	$⊢ (x = C \land r = W (B) \cap (C \times C)) \to x = C$
58	57	sseq1d	$⊢ (x = C \land r = W (B) \cap (C \times C)) \to (x \subseteq A \leftrightarrow C \subseteq A)$
59		simpr	$⊢ (x = C \land r = W (B) \cap (C \times C)) \to r = W (B) \cap (C \times C)$
60	57	sqxpeqd	$⊢ (x = C \land r = W (B) \cap (C \times C)) \to x \times x = C \times C$
61	59 60	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)$
62	59 57	weeq12d	$⊢ (x = C \land r = W (B) \cap (C \times C)) \to (r We x \leftrightarrow (W (B) \cap (C \times C)) We C)$
63	58 61 62	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))$
64	55 56 63	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)$
65	43 45 51 64	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)\}$
66	65 1	eleqtrrdi	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to ⟨C, W (B) \cap (C \times C)⟩ \in O$
67	8 42	ssexd	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to B \in V$
68	52	a1i	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to W (B) \in V$
69		simpl	$⊢ (x = B \land r = W (B)) \to x = B$
70	69	sseq1d	$⊢ (x = B \land r = W (B)) \to (x \subseteq A \leftrightarrow B \subseteq A)$
71		simpr	$⊢ (x = B \land r = W (B)) \to r = W (B)$
72	69	sqxpeqd	$⊢ (x = B \land r = W (B)) \to x \times x = B \times B$
73	71 72	sseq12d	$⊢ (x = B \land r = W (B)) \to (r \subseteq x \times x \leftrightarrow W (B) \subseteq B \times B)$
74	71 69	weeq12d	$⊢ (x = B \land r = W (B)) \to (r We x \leftrightarrow W (B) We B)$
75	70 73 74	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))$
76	75	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))$
77	67 68 76	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))$
78	42 35 47 77	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)\}$
79	78 1	eleqtrrdi	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to ⟨B, W (B)⟩ \in O$
80		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)⟩)$
81	30 66 79 80	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)⟩)$
82	29 81	mpbid	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to ⟨C, W (B) \cap (C \times C)⟩ = ⟨B, W (B)⟩$
83	55 56	opth1	$⊢ ⟨C, W (B) \cap (C \times C)⟩ = ⟨B, W (B)⟩ \to C = B$
84	82 83	syl	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to C = B$
85	19 84	eleqtrrd	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to B F W (B) \in C$
86	85 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)\}]$
87		ovex	$⊢ B F W (B) \in V$
88	87	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)))$
89	19 88	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)))$
90	86 89	mpbid	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to (B F W (B)) W (B) (B F W (B))$
91		weso	$⊢ W (B) We B \to W (B) Or B$
92	47 91	syl	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to W (B) Or B$
93		sonr	$⊢ (W (B) Or B \land B F W (B) \in B) \to \neg (B F W (B)) W (B) (B F W (B))$
94	92 19 93	syl2anc	$⊢ (A \in V \land F : O \underset{1-1}{⟶} A) \to \neg (B F W (B)) W (B) (B F W (B))$
95	90 94	pm2.65da	$⊢ A \in V \to \neg F : O \underset{1-1}{⟶} A$

Metamath Proof Explorer

Theorem canthwelem

Proof