pwfseqlem4

Description: Lemma for pwfseq . Derive a final contradiction from the function F in pwfseqlem3 . Applying fpwwe2 to it, we get a certain maximal well-ordered subset Z , but the defining property ( Z F ( WZ ) ) e. Z contradicts our assumption on F , so we are reduced to the case of Z finite. This too is a contradiction, though, because Z and its preimage under ( WZ ) are distinct sets of the same cardinality and in a subset relation, which is impossible for finite sets. (Contributed by Mario Carneiro, 31-May-2015)

	Ref	Expression
Hypotheses	pwfseqlem4.g	$⊢ φ \to G : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n})$
	pwfseqlem4.x	$⊢ φ \to X \subseteq A$
	pwfseqlem4.h	$⊢ φ \to H : ω \underset{1-1 onto}{⟶} X$
	pwfseqlem4.ps	$⊢ ψ \leftrightarrow ((x \subseteq A \land r \subseteq x \times x \land r We x) \land ω ≼ x)$
	pwfseqlem4.k	$⊢ (φ \land ψ) \to K : ⋃_{n \in ω} (x^{n}) \underset{1-1}{⟶} x$
	pwfseqlem4.d	$⊢ D = G (\{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\})$
	pwfseqlem4.f	$⊢ F = (x \in V, r \in V ⟼ if (x \in Fin, H (card (x)), D (⋂ \{z \in ω \| \neg D (z) \in x\})))$
	pwfseqlem4.w	$⊢ W = \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall b \in a \underset{˙}{[} s^{-1} [\{b\}] / v \underset{˙}{]} v F (s \cap (v \times v)) = b))\}$
	pwfseqlem4.z	$⊢ Z = ⋃ dom W$
Assertion	pwfseqlem4	$⊢ \neg φ$

Proof

Step	Hyp	Ref	Expression
1		pwfseqlem4.g	$⊢ φ \to G : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n})$
2		pwfseqlem4.x	$⊢ φ \to X \subseteq A$
3		pwfseqlem4.h	$⊢ φ \to H : ω \underset{1-1 onto}{⟶} X$
4		pwfseqlem4.ps	$⊢ ψ \leftrightarrow ((x \subseteq A \land r \subseteq x \times x \land r We x) \land ω ≼ x)$
5		pwfseqlem4.k	$⊢ (φ \land ψ) \to K : ⋃_{n \in ω} (x^{n}) \underset{1-1}{⟶} x$
6		pwfseqlem4.d	$⊢ D = G (\{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\})$
7		pwfseqlem4.f	$⊢ F = (x \in V, r \in V ⟼ if (x \in Fin, H (card (x)), D (⋂ \{z \in ω \| \neg D (z) \in x\})))$
8		pwfseqlem4.w	$⊢ W = \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall b \in a \underset{˙}{[} s^{-1} [\{b\}] / v \underset{˙}{]} v F (s \cap (v \times v)) = b))\}$
9		pwfseqlem4.z	$⊢ Z = ⋃ dom W$
10		eqid	$⊢ Z = Z$
11		eqid	$⊢ W (Z) = W (Z)$
12	10 11	pm3.2i	$⊢ (Z = Z \land W (Z) = W (Z))$
13		omex	$⊢ ω \in V$
14		ovex	$⊢ A^{n} \in V$
15	13 14	iunex	$⊢ ⋃_{n \in ω} (A^{n}) \in V$
16		f1dmex	$⊢ (G : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n}) \land ⋃_{n \in ω} (A^{n}) \in V) \to 𝒫 A \in V$
17	1 15 16	sylancl	$⊢ φ \to 𝒫 A \in V$
18		pwexb	$⊢ A \in V \leftrightarrow 𝒫 A \in V$
19	17 18	sylibr	$⊢ φ \to A \in V$
20	1 2 3 4 5 6 7	pwfseqlem4a	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to a F s \in A$
21	8 19 20 9	fpwwe2	$⊢ φ \to ((Z W W (Z) \land Z F W (Z) \in Z) \leftrightarrow (Z = Z \land W (Z) = W (Z)))$
22	12 21	mpbiri	$⊢ φ \to (Z W W (Z) \land Z F W (Z) \in Z)$
23	22	simprd	$⊢ φ \to Z F W (Z) \in Z$
24	22	simpld	$⊢ φ \to Z W W (Z)$
25	8 19	fpwwe2lem2	$⊢ φ \to (Z W W (Z) \leftrightarrow ((Z \subseteq A \land W (Z) \subseteq Z \times Z) \land (W (Z) We Z \land \forall b \in Z \underset{˙}{[} {W (Z)}^{-1} [\{b\}] / v \underset{˙}{]} v F (W (Z) \cap (v \times v)) = b)))$
26	24 25	mpbid	$⊢ φ \to ((Z \subseteq A \land W (Z) \subseteq Z \times Z) \land (W (Z) We Z \land \forall b \in Z \underset{˙}{[} {W (Z)}^{-1} [\{b\}] / v \underset{˙}{]} v F (W (Z) \cap (v \times v)) = b))$
27	26	simpld	$⊢ φ \to (Z \subseteq A \land W (Z) \subseteq Z \times Z)$
28	27	simpld	$⊢ φ \to Z \subseteq A$
29	19 28	ssexd	$⊢ φ \to Z \in V$
30		sseq1	$⊢ a = Z \to (a \subseteq A \leftrightarrow Z \subseteq A)$
31		id	$⊢ a = Z \to a = Z$
32	31	sqxpeqd	$⊢ a = Z \to a \times a = Z \times Z$
33	32	sseq2d	$⊢ a = Z \to (W (Z) \subseteq a \times a \leftrightarrow W (Z) \subseteq Z \times Z)$
34		weeq2	$⊢ a = Z \to (W (Z) We a \leftrightarrow W (Z) We Z)$
35	30 33 34	3anbi123d	$⊢ a = Z \to ((a \subseteq A \land W (Z) \subseteq a \times a \land W (Z) We a) \leftrightarrow (Z \subseteq A \land W (Z) \subseteq Z \times Z \land W (Z) We Z))$
36	35	anbi2d	$⊢ a = Z \to ((φ \land (a \subseteq A \land W (Z) \subseteq a \times a \land W (Z) We a)) \leftrightarrow (φ \land (Z \subseteq A \land W (Z) \subseteq Z \times Z \land W (Z) We Z)))$
37		id	$⊢ (Z \subseteq A \land W (Z) \subseteq Z \times Z \land W (Z) We Z) \to (Z \subseteq A \land W (Z) \subseteq Z \times Z \land W (Z) We Z)$
38	37	3expa	$⊢ ((Z \subseteq A \land W (Z) \subseteq Z \times Z) \land W (Z) We Z) \to (Z \subseteq A \land W (Z) \subseteq Z \times Z \land W (Z) We Z)$
39	38	adantrr	$⊢ ((Z \subseteq A \land W (Z) \subseteq Z \times Z) \land (W (Z) We Z \land \forall b \in Z \underset{˙}{[} {W (Z)}^{-1} [\{b\}] / v \underset{˙}{]} v F (W (Z) \cap (v \times v)) = b)) \to (Z \subseteq A \land W (Z) \subseteq Z \times Z \land W (Z) We Z)$
40	26 39	syl	$⊢ φ \to (Z \subseteq A \land W (Z) \subseteq Z \times Z \land W (Z) We Z)$
41	40	pm4.71i	$⊢ φ \leftrightarrow (φ \land (Z \subseteq A \land W (Z) \subseteq Z \times Z \land W (Z) We Z))$
42	36 41	bitr4di	$⊢ a = Z \to ((φ \land (a \subseteq A \land W (Z) \subseteq a \times a \land W (Z) We a)) \leftrightarrow φ)$
43		oveq1	$⊢ a = Z \to a F W (Z) = Z F W (Z)$
44	43 31	eleq12d	$⊢ a = Z \to (a F W (Z) \in a \leftrightarrow Z F W (Z) \in Z)$
45		breq1	$⊢ a = Z \to (a ≺ ω \leftrightarrow Z ≺ ω)$
46	44 45	imbi12d	$⊢ a = Z \to ((a F W (Z) \in a \to a ≺ ω) \leftrightarrow (Z F W (Z) \in Z \to Z ≺ ω))$
47	42 46	imbi12d	$⊢ a = Z \to (((φ \land (a \subseteq A \land W (Z) \subseteq a \times a \land W (Z) We a)) \to (a F W (Z) \in a \to a ≺ ω)) \leftrightarrow (φ \to (Z F W (Z) \in Z \to Z ≺ ω)))$
48		fvex	$⊢ W (Z) \in V$
49		sseq1	$⊢ s = W (Z) \to (s \subseteq a \times a \leftrightarrow W (Z) \subseteq a \times a)$
50		weeq1	$⊢ s = W (Z) \to (s We a \leftrightarrow W (Z) We a)$
51	49 50	3anbi23d	$⊢ s = W (Z) \to ((a \subseteq A \land s \subseteq a \times a \land s We a) \leftrightarrow (a \subseteq A \land W (Z) \subseteq a \times a \land W (Z) We a))$
52	51	anbi2d	$⊢ s = W (Z) \to ((φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \leftrightarrow (φ \land (a \subseteq A \land W (Z) \subseteq a \times a \land W (Z) We a)))$
53		oveq2	$⊢ s = W (Z) \to a F s = a F W (Z)$
54	53	eleq1d	$⊢ s = W (Z) \to (a F s \in a \leftrightarrow a F W (Z) \in a)$
55	54	imbi1d	$⊢ s = W (Z) \to ((a F s \in a \to a ≺ ω) \leftrightarrow (a F W (Z) \in a \to a ≺ ω))$
56	52 55	imbi12d	$⊢ s = W (Z) \to (((φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to (a F s \in a \to a ≺ ω)) \leftrightarrow ((φ \land (a \subseteq A \land W (Z) \subseteq a \times a \land W (Z) We a)) \to (a F W (Z) \in a \to a ≺ ω)))$
57		omelon	$⊢ ω \in On$
58		onenon	$⊢ ω \in On \to ω \in dom card$
59	57 58	ax-mp	$⊢ ω \in dom card$
60		simpr3	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to s We a$
61	60	19.8ad	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to \exists s s We a$
62		ween	$⊢ a \in dom card \leftrightarrow \exists s s We a$
63	61 62	sylibr	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to a \in dom card$
64		domtri2	$⊢ (ω \in dom card \land a \in dom card) \to (ω ≼ a \leftrightarrow \neg a ≺ ω)$
65	59 63 64	sylancr	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to (ω ≼ a \leftrightarrow \neg a ≺ ω)$
66		nfv	$⊢ Ⅎ r (φ \land ((a \subseteq A \land s \subseteq a \times a \land s We a) \land ω ≼ a))$
67		nfcv	$⊢ \underline{Ⅎ} r a$
68		nfmpo2	$⊢ \underline{Ⅎ} r (x \in V, r \in V ⟼ if (x \in Fin, H (card (x)), D (⋂ \{z \in ω \| \neg D (z) \in x\})))$
69	7 68	nfcxfr	$⊢ \underline{Ⅎ} r F$
70		nfcv	$⊢ \underline{Ⅎ} r s$
71	67 69 70	nfov	$⊢ \underline{Ⅎ} r (a F s)$
72	71	nfel1	$⊢ Ⅎ r a F s \in (A ∖ a)$
73	66 72	nfim	$⊢ Ⅎ r ((φ \land ((a \subseteq A \land s \subseteq a \times a \land s We a) \land ω ≼ a)) \to a F s \in (A ∖ a))$
74		sseq1	$⊢ r = s \to (r \subseteq a \times a \leftrightarrow s \subseteq a \times a)$
75		weeq1	$⊢ r = s \to (r We a \leftrightarrow s We a)$
76	74 75	3anbi23d	$⊢ r = s \to ((a \subseteq A \land r \subseteq a \times a \land r We a) \leftrightarrow (a \subseteq A \land s \subseteq a \times a \land s We a))$
77	76	anbi1d	$⊢ r = s \to (((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a) \leftrightarrow ((a \subseteq A \land s \subseteq a \times a \land s We a) \land ω ≼ a))$
78	77	anbi2d	$⊢ r = s \to ((φ \land ((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a)) \leftrightarrow (φ \land ((a \subseteq A \land s \subseteq a \times a \land s We a) \land ω ≼ a)))$
79		oveq2	$⊢ r = s \to a F r = a F s$
80	79	eleq1d	$⊢ r = s \to (a F r \in (A ∖ a) \leftrightarrow a F s \in (A ∖ a))$
81	78 80	imbi12d	$⊢ r = s \to (((φ \land ((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a)) \to a F r \in (A ∖ a)) \leftrightarrow ((φ \land ((a \subseteq A \land s \subseteq a \times a \land s We a) \land ω ≼ a)) \to a F s \in (A ∖ a)))$
82		nfv	$⊢ Ⅎ x (φ \land ((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a))$
83		nfcv	$⊢ \underline{Ⅎ} x a$
84		nfmpo1	$⊢ \underline{Ⅎ} x (x \in V, r \in V ⟼ if (x \in Fin, H (card (x)), D (⋂ \{z \in ω \| \neg D (z) \in x\})))$
85	7 84	nfcxfr	$⊢ \underline{Ⅎ} x F$
86		nfcv	$⊢ \underline{Ⅎ} x r$
87	83 85 86	nfov	$⊢ \underline{Ⅎ} x (a F r)$
88	87	nfel1	$⊢ Ⅎ x a F r \in (A ∖ a)$
89	82 88	nfim	$⊢ Ⅎ x ((φ \land ((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a)) \to a F r \in (A ∖ a))$
90		sseq1	$⊢ x = a \to (x \subseteq A \leftrightarrow a \subseteq A)$
91		xpeq12	$⊢ (x = a \land x = a) \to x \times x = a \times a$
92	91	anidms	$⊢ x = a \to x \times x = a \times a$
93	92	sseq2d	$⊢ x = a \to (r \subseteq x \times x \leftrightarrow r \subseteq a \times a)$
94		weeq2	$⊢ x = a \to (r We x \leftrightarrow r We a)$
95	90 93 94	3anbi123d	$⊢ x = a \to ((x \subseteq A \land r \subseteq x \times x \land r We x) \leftrightarrow (a \subseteq A \land r \subseteq a \times a \land r We a))$
96		breq2	$⊢ x = a \to (ω ≼ x \leftrightarrow ω ≼ a)$
97	95 96	anbi12d	$⊢ x = a \to (((x \subseteq A \land r \subseteq x \times x \land r We x) \land ω ≼ x) \leftrightarrow ((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a))$
98	4 97	syl5bb	$⊢ x = a \to (ψ \leftrightarrow ((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a))$
99	98	anbi2d	$⊢ x = a \to ((φ \land ψ) \leftrightarrow (φ \land ((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a)))$
100		oveq1	$⊢ x = a \to x F r = a F r$
101		difeq2	$⊢ x = a \to A ∖ x = A ∖ a$
102	100 101	eleq12d	$⊢ x = a \to (x F r \in (A ∖ x) \leftrightarrow a F r \in (A ∖ a))$
103	99 102	imbi12d	$⊢ x = a \to (((φ \land ψ) \to x F r \in (A ∖ x)) \leftrightarrow ((φ \land ((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a)) \to a F r \in (A ∖ a)))$
104	1 2 3 4 5 6 7	pwfseqlem3	$⊢ (φ \land ψ) \to x F r \in (A ∖ x)$
105	89 103 104	chvarfv	$⊢ (φ \land ((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a)) \to a F r \in (A ∖ a)$
106	73 81 105	chvarfv	$⊢ (φ \land ((a \subseteq A \land s \subseteq a \times a \land s We a) \land ω ≼ a)) \to a F s \in (A ∖ a)$
107	106	eldifbd	$⊢ (φ \land ((a \subseteq A \land s \subseteq a \times a \land s We a) \land ω ≼ a)) \to \neg a F s \in a$
108	107	expr	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to (ω ≼ a \to \neg a F s \in a)$
109	65 108	sylbird	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to (\neg a ≺ ω \to \neg a F s \in a)$
110	109	con4d	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to (a F s \in a \to a ≺ ω)$
111	48 56 110	vtocl	$⊢ (φ \land (a \subseteq A \land W (Z) \subseteq a \times a \land W (Z) We a)) \to (a F W (Z) \in a \to a ≺ ω)$
112	47 111	vtoclg	$⊢ Z \in V \to (φ \to (Z F W (Z) \in Z \to Z ≺ ω))$
113	29 112	mpcom	$⊢ φ \to (Z F W (Z) \in Z \to Z ≺ ω)$
114	23 113	mpd	$⊢ φ \to Z ≺ ω$
115		isfinite	$⊢ Z \in Fin \leftrightarrow Z ≺ ω$
116	114 115	sylibr	$⊢ φ \to Z \in Fin$
117	1 2 3 4 5 6 7	pwfseqlem2	$⊢ (Z \in Fin \land W (Z) \in V) \to Z F W (Z) = H (card (Z))$
118	116 48 117	sylancl	$⊢ φ \to Z F W (Z) = H (card (Z))$
119	118 23	eqeltrrd	$⊢ φ \to H (card (Z)) \in Z$
120	8 19 24	fpwwe2lem3	$⊢ (φ \land H (card (Z)) \in Z) \to {W (Z)}^{-1} [\{H (card (Z))\}] F (W (Z) \cap ({W (Z)}^{-1} [\{H (card (Z))\}] \times {W (Z)}^{-1} [\{H (card (Z))\}])) = H (card (Z))$
121	119 120	mpdan	$⊢ φ \to {W (Z)}^{-1} [\{H (card (Z))\}] F (W (Z) \cap ({W (Z)}^{-1} [\{H (card (Z))\}] \times {W (Z)}^{-1} [\{H (card (Z))\}])) = H (card (Z))$
122		cnvimass	$⊢ {W (Z)}^{-1} [\{H (card (Z))\}] \subseteq dom W (Z)$
123	27	simprd	$⊢ φ \to W (Z) \subseteq Z \times Z$
124		dmss	$⊢ W (Z) \subseteq Z \times Z \to dom W (Z) \subseteq dom (Z \times Z)$
125	123 124	syl	$⊢ φ \to dom W (Z) \subseteq dom (Z \times Z)$
126		dmxpss	$⊢ dom (Z \times Z) \subseteq Z$
127	125 126	sstrdi	$⊢ φ \to dom W (Z) \subseteq Z$
128	122 127	sstrid	$⊢ φ \to {W (Z)}^{-1} [\{H (card (Z))\}] \subseteq Z$
129	116 128	ssfid	$⊢ φ \to {W (Z)}^{-1} [\{H (card (Z))\}] \in Fin$
130	48	inex1	$⊢ W (Z) \cap ({W (Z)}^{-1} [\{H (card (Z))\}] \times {W (Z)}^{-1} [\{H (card (Z))\}]) \in V$
131	1 2 3 4 5 6 7	pwfseqlem2	$⊢ ({W (Z)}^{-1} [\{H (card (Z))\}] \in Fin \land W (Z) \cap ({W (Z)}^{-1} [\{H (card (Z))\}] \times {W (Z)}^{-1} [\{H (card (Z))\}]) \in V) \to {W (Z)}^{-1} [\{H (card (Z))\}] F (W (Z) \cap ({W (Z)}^{-1} [\{H (card (Z))\}] \times {W (Z)}^{-1} [\{H (card (Z))\}])) = H (card ({W (Z)}^{-1} [\{H (card (Z))\}]))$
132	129 130 131	sylancl	$⊢ φ \to {W (Z)}^{-1} [\{H (card (Z))\}] F (W (Z) \cap ({W (Z)}^{-1} [\{H (card (Z))\}] \times {W (Z)}^{-1} [\{H (card (Z))\}])) = H (card ({W (Z)}^{-1} [\{H (card (Z))\}]))$
133	121 132	eqtr3d	$⊢ φ \to H (card (Z)) = H (card ({W (Z)}^{-1} [\{H (card (Z))\}]))$
134		f1of1	$⊢ H : ω \underset{1-1 onto}{⟶} X \to H : ω \underset{1-1}{⟶} X$
135	3 134	syl	$⊢ φ \to H : ω \underset{1-1}{⟶} X$
136		ficardom	$⊢ Z \in Fin \to card (Z) \in ω$
137	116 136	syl	$⊢ φ \to card (Z) \in ω$
138		ficardom	$⊢ {W (Z)}^{-1} [\{H (card (Z))\}] \in Fin \to card ({W (Z)}^{-1} [\{H (card (Z))\}]) \in ω$
139	129 138	syl	$⊢ φ \to card ({W (Z)}^{-1} [\{H (card (Z))\}]) \in ω$
140		f1fveq	$⊢ (H : ω \underset{1-1}{⟶} X \land (card (Z) \in ω \land card ({W (Z)}^{-1} [\{H (card (Z))\}]) \in ω)) \to (H (card (Z)) = H (card ({W (Z)}^{-1} [\{H (card (Z))\}])) \leftrightarrow card (Z) = card ({W (Z)}^{-1} [\{H (card (Z))\}]))$
141	135 137 139 140	syl12anc	$⊢ φ \to (H (card (Z)) = H (card ({W (Z)}^{-1} [\{H (card (Z))\}])) \leftrightarrow card (Z) = card ({W (Z)}^{-1} [\{H (card (Z))\}]))$
142	133 141	mpbid	$⊢ φ \to card (Z) = card ({W (Z)}^{-1} [\{H (card (Z))\}])$
143	142	eqcomd	$⊢ φ \to card ({W (Z)}^{-1} [\{H (card (Z))\}]) = card (Z)$
144		finnum	$⊢ {W (Z)}^{-1} [\{H (card (Z))\}] \in Fin \to {W (Z)}^{-1} [\{H (card (Z))\}] \in dom card$
145	129 144	syl	$⊢ φ \to {W (Z)}^{-1} [\{H (card (Z))\}] \in dom card$
146		finnum	$⊢ Z \in Fin \to Z \in dom card$
147	116 146	syl	$⊢ φ \to Z \in dom card$
148		carden2	$⊢ ({W (Z)}^{-1} [\{H (card (Z))\}] \in dom card \land Z \in dom card) \to (card ({W (Z)}^{-1} [\{H (card (Z))\}]) = card (Z) \leftrightarrow {W (Z)}^{-1} [\{H (card (Z))\}] \approx Z)$
149	145 147 148	syl2anc	$⊢ φ \to (card ({W (Z)}^{-1} [\{H (card (Z))\}]) = card (Z) \leftrightarrow {W (Z)}^{-1} [\{H (card (Z))\}] \approx Z)$
150	143 149	mpbid	$⊢ φ \to {W (Z)}^{-1} [\{H (card (Z))\}] \approx Z$
151		dfpss2	$⊢ {W (Z)}^{-1} [\{H (card (Z))\}] \subset Z \leftrightarrow ({W (Z)}^{-1} [\{H (card (Z))\}] \subseteq Z \land \neg {W (Z)}^{-1} [\{H (card (Z))\}] = Z)$
152	151	baib	$⊢ {W (Z)}^{-1} [\{H (card (Z))\}] \subseteq Z \to ({W (Z)}^{-1} [\{H (card (Z))\}] \subset Z \leftrightarrow \neg {W (Z)}^{-1} [\{H (card (Z))\}] = Z)$
153	128 152	syl	$⊢ φ \to ({W (Z)}^{-1} [\{H (card (Z))\}] \subset Z \leftrightarrow \neg {W (Z)}^{-1} [\{H (card (Z))\}] = Z)$
154		php3	$⊢ (Z \in Fin \land {W (Z)}^{-1} [\{H (card (Z))\}] \subset Z) \to {W (Z)}^{-1} [\{H (card (Z))\}] ≺ Z$
155		sdomnen	$⊢ {W (Z)}^{-1} [\{H (card (Z))\}] ≺ Z \to \neg {W (Z)}^{-1} [\{H (card (Z))\}] \approx Z$
156	154 155	syl	$⊢ (Z \in Fin \land {W (Z)}^{-1} [\{H (card (Z))\}] \subset Z) \to \neg {W (Z)}^{-1} [\{H (card (Z))\}] \approx Z$
157	156	ex	$⊢ Z \in Fin \to ({W (Z)}^{-1} [\{H (card (Z))\}] \subset Z \to \neg {W (Z)}^{-1} [\{H (card (Z))\}] \approx Z)$
158	116 157	syl	$⊢ φ \to ({W (Z)}^{-1} [\{H (card (Z))\}] \subset Z \to \neg {W (Z)}^{-1} [\{H (card (Z))\}] \approx Z)$
159	153 158	sylbird	$⊢ φ \to (\neg {W (Z)}^{-1} [\{H (card (Z))\}] = Z \to \neg {W (Z)}^{-1} [\{H (card (Z))\}] \approx Z)$
160	150 159	mt4d	$⊢ φ \to {W (Z)}^{-1} [\{H (card (Z))\}] = Z$
161	119 160	eleqtrrd	$⊢ φ \to H (card (Z)) \in {W (Z)}^{-1} [\{H (card (Z))\}]$
162		fvex	$⊢ H (card (Z)) \in V$
163	162	eliniseg	$⊢ H (card (Z)) \in V \to (H (card (Z)) \in {W (Z)}^{-1} [\{H (card (Z))\}] \leftrightarrow H (card (Z)) W (Z) H (card (Z)))$
164	162 163	ax-mp	$⊢ H (card (Z)) \in {W (Z)}^{-1} [\{H (card (Z))\}] \leftrightarrow H (card (Z)) W (Z) H (card (Z))$
165	161 164	sylib	$⊢ φ \to H (card (Z)) W (Z) H (card (Z))$
166	26	simprd	$⊢ φ \to (W (Z) We Z \land \forall b \in Z \underset{˙}{[} {W (Z)}^{-1} [\{b\}] / v \underset{˙}{]} v F (W (Z) \cap (v \times v)) = b)$
167	166	simpld	$⊢ φ \to W (Z) We Z$
168		weso	$⊢ W (Z) We Z \to W (Z) Or Z$
169	167 168	syl	$⊢ φ \to W (Z) Or Z$
170		sonr	$⊢ (W (Z) Or Z \land H (card (Z)) \in Z) \to \neg H (card (Z)) W (Z) H (card (Z))$
171	169 119 170	syl2anc	$⊢ φ \to \neg H (card (Z)) W (Z) H (card (Z))$
172	165 171	pm2.65i	$⊢ \neg φ$

Metamath Proof Explorer

Theorem pwfseqlem4

Proof