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) (Proof shortened by Matthew House, 10-Sep-2025)

	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	simpld	$⊢ φ \to Z W W (Z)$
24	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)))$
25	23 24	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))$
26		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)$
27	26	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)$
28	27	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)$
29	25 28	syl	$⊢ φ \to (Z \subseteq A \land W (Z) \subseteq Z \times Z \land W (Z) We Z)$
30	22	simprd	$⊢ φ \to Z F W (Z) \in Z$
31	25	simpld	$⊢ φ \to (Z \subseteq A \land W (Z) \subseteq Z \times Z)$
32	31	simpld	$⊢ φ \to Z \subseteq A$
33	19 32	ssexd	$⊢ φ \to Z \in V$
34		fvexd	$⊢ φ \to W (Z) \in V$
35		simpl	$⊢ (a = Z \land s = W (Z)) \to a = Z$
36	35	sseq1d	$⊢ (a = Z \land s = W (Z)) \to (a \subseteq A \leftrightarrow Z \subseteq A)$
37		simpr	$⊢ (a = Z \land s = W (Z)) \to s = W (Z)$
38	35	sqxpeqd	$⊢ (a = Z \land s = W (Z)) \to a \times a = Z \times Z$
39	37 38	sseq12d	$⊢ (a = Z \land s = W (Z)) \to (s \subseteq a \times a \leftrightarrow W (Z) \subseteq Z \times Z)$
40	37 35	weeq12d	$⊢ (a = Z \land s = W (Z)) \to (s We a \leftrightarrow W (Z) We Z)$
41	36 39 40	3anbi123d	$⊢ (a = Z \land s = W (Z)) \to ((a \subseteq A \land s \subseteq a \times a \land s We a) \leftrightarrow (Z \subseteq A \land W (Z) \subseteq Z \times Z \land W (Z) We Z))$
42		oveq12	$⊢ (a = Z \land s = W (Z)) \to a F s = Z F W (Z)$
43	42 35	eleq12d	$⊢ (a = Z \land s = W (Z)) \to (a F s \in a \leftrightarrow Z F W (Z) \in Z)$
44	35	breq1d	$⊢ (a = Z \land s = W (Z)) \to (a ≺ ω \leftrightarrow Z ≺ ω)$
45	43 44	imbi12d	$⊢ (a = Z \land s = W (Z)) \to ((a F s \in a \to a ≺ ω) \leftrightarrow (Z F W (Z) \in Z \to Z ≺ ω))$
46	41 45	imbi12d	$⊢ (a = Z \land s = W (Z)) \to (((a \subseteq A \land s \subseteq a \times a \land s We a) \to (a F s \in a \to a ≺ ω)) \leftrightarrow ((Z \subseteq A \land W (Z) \subseteq Z \times Z \land W (Z) We Z) \to (Z F W (Z) \in Z \to Z ≺ ω)))$
47		omelon	$⊢ ω \in On$
48		onenon	$⊢ ω \in On \to ω \in dom card$
49	47 48	ax-mp	$⊢ ω \in dom card$
50		simpr3	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to s We a$
51	50	19.8ad	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to \exists s s We a$
52		ween	$⊢ a \in dom card \leftrightarrow \exists s s We a$
53	51 52	sylibr	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to a \in dom card$
54		domtri2	$⊢ (ω \in dom card \land a \in dom card) \to (ω ≼ a \leftrightarrow \neg a ≺ ω)$
55	49 53 54	sylancr	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to (ω ≼ a \leftrightarrow \neg a ≺ ω)$
56		nfv	$⊢ Ⅎ r (φ \land ((a \subseteq A \land s \subseteq a \times a \land s We a) \land ω ≼ a))$
57		nfcv	$⊢ \underline{Ⅎ} r a$
58		nfmpo2	$⊢ \underline{Ⅎ} r (x \in V, r \in V ⟼ if (x \in Fin, H (card (x)), D (⋂ \{z \in ω \| \neg D (z) \in x\})))$
59	7 58	nfcxfr	$⊢ \underline{Ⅎ} r F$
60		nfcv	$⊢ \underline{Ⅎ} r s$
61	57 59 60	nfov	$⊢ \underline{Ⅎ} r (a F s)$
62	61	nfel1	$⊢ Ⅎ r a F s \in (A ∖ a)$
63	56 62	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))$
64		sseq1	$⊢ r = s \to (r \subseteq a \times a \leftrightarrow s \subseteq a \times a)$
65		weeq1	$⊢ r = s \to (r We a \leftrightarrow s We a)$
66	64 65	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))$
67	66	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))$
68	67	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)))$
69		oveq2	$⊢ r = s \to a F r = a F s$
70	69	eleq1d	$⊢ r = s \to (a F r \in (A ∖ a) \leftrightarrow a F s \in (A ∖ a))$
71	68 70	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)))$
72		nfv	$⊢ Ⅎ x (φ \land ((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a))$
73		nfcv	$⊢ \underline{Ⅎ} x a$
74		nfmpo1	$⊢ \underline{Ⅎ} x (x \in V, r \in V ⟼ if (x \in Fin, H (card (x)), D (⋂ \{z \in ω \| \neg D (z) \in x\})))$
75	7 74	nfcxfr	$⊢ \underline{Ⅎ} x F$
76		nfcv	$⊢ \underline{Ⅎ} x r$
77	73 75 76	nfov	$⊢ \underline{Ⅎ} x (a F r)$
78	77	nfel1	$⊢ Ⅎ x a F r \in (A ∖ a)$
79	72 78	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))$
80		sseq1	$⊢ x = a \to (x \subseteq A \leftrightarrow a \subseteq A)$
81		xpeq12	$⊢ (x = a \land x = a) \to x \times x = a \times a$
82	81	anidms	$⊢ x = a \to x \times x = a \times a$
83	82	sseq2d	$⊢ x = a \to (r \subseteq x \times x \leftrightarrow r \subseteq a \times a)$
84		weeq2	$⊢ x = a \to (r We x \leftrightarrow r We a)$
85	80 83 84	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))$
86		breq2	$⊢ x = a \to (ω ≼ x \leftrightarrow ω ≼ a)$
87	85 86	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))$
88	4 87	bitrid	$⊢ x = a \to (ψ \leftrightarrow ((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a))$
89	88	anbi2d	$⊢ x = a \to ((φ \land ψ) \leftrightarrow (φ \land ((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a)))$
90		oveq1	$⊢ x = a \to x F r = a F r$
91		difeq2	$⊢ x = a \to A ∖ x = A ∖ a$
92	90 91	eleq12d	$⊢ x = a \to (x F r \in (A ∖ x) \leftrightarrow a F r \in (A ∖ a))$
93	89 92	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)))$
94	1 2 3 4 5 6 7	pwfseqlem3	$⊢ (φ \land ψ) \to x F r \in (A ∖ x)$
95	79 93 94	chvarfv	$⊢ (φ \land ((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a)) \to a F r \in (A ∖ a)$
96	63 71 95	chvarfv	$⊢ (φ \land ((a \subseteq A \land s \subseteq a \times a \land s We a) \land ω ≼ a)) \to a F s \in (A ∖ a)$
97	96	eldifbd	$⊢ (φ \land ((a \subseteq A \land s \subseteq a \times a \land s We a) \land ω ≼ a)) \to \neg a F s \in a$
98	97	expr	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to (ω ≼ a \to \neg a F s \in a)$
99	55 98	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)$
100	99	con4d	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to (a F s \in a \to a ≺ ω)$
101	100	ex	$⊢ φ \to ((a \subseteq A \land s \subseteq a \times a \land s We a) \to (a F s \in a \to a ≺ ω))$
102	33 34 46 101	vtocl2d	$⊢ φ \to ((Z \subseteq A \land W (Z) \subseteq Z \times Z \land W (Z) We Z) \to (Z F W (Z) \in Z \to Z ≺ ω))$
103	29 30 102	mp2d	$⊢ φ \to Z ≺ ω$
104		isfinite	$⊢ Z \in Fin \leftrightarrow Z ≺ ω$
105	103 104	sylibr	$⊢ φ \to Z \in Fin$
106		fvex	$⊢ W (Z) \in V$
107	1 2 3 4 5 6 7	pwfseqlem2	$⊢ (Z \in Fin \land W (Z) \in V) \to Z F W (Z) = H (card (Z))$
108	105 106 107	sylancl	$⊢ φ \to Z F W (Z) = H (card (Z))$
109	108 30	eqeltrrd	$⊢ φ \to H (card (Z)) \in Z$
110	8 19 23	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))$
111	109 110	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))$
112		cnvimass	$⊢ {W (Z)}^{-1} [\{H (card (Z))\}] \subseteq dom W (Z)$
113	31	simprd	$⊢ φ \to W (Z) \subseteq Z \times Z$
114		dmss	$⊢ W (Z) \subseteq Z \times Z \to dom W (Z) \subseteq dom (Z \times Z)$
115	113 114	syl	$⊢ φ \to dom W (Z) \subseteq dom (Z \times Z)$
116		dmxpss	$⊢ dom (Z \times Z) \subseteq Z$
117	115 116	sstrdi	$⊢ φ \to dom W (Z) \subseteq Z$
118	112 117	sstrid	$⊢ φ \to {W (Z)}^{-1} [\{H (card (Z))\}] \subseteq Z$
119	105 118	ssfid	$⊢ φ \to {W (Z)}^{-1} [\{H (card (Z))\}] \in Fin$
120	106	inex1	$⊢ W (Z) \cap ({W (Z)}^{-1} [\{H (card (Z))\}] \times {W (Z)}^{-1} [\{H (card (Z))\}]) \in V$
121	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))\}]))$
122	119 120 121	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))\}]))$
123	111 122	eqtr3d	$⊢ φ \to H (card (Z)) = H (card ({W (Z)}^{-1} [\{H (card (Z))\}]))$
124		f1of1	$⊢ H : ω \underset{1-1 onto}{⟶} X \to H : ω \underset{1-1}{⟶} X$
125	3 124	syl	$⊢ φ \to H : ω \underset{1-1}{⟶} X$
126		ficardom	$⊢ Z \in Fin \to card (Z) \in ω$
127	105 126	syl	$⊢ φ \to card (Z) \in ω$
128		ficardom	$⊢ {W (Z)}^{-1} [\{H (card (Z))\}] \in Fin \to card ({W (Z)}^{-1} [\{H (card (Z))\}]) \in ω$
129	119 128	syl	$⊢ φ \to card ({W (Z)}^{-1} [\{H (card (Z))\}]) \in ω$
130		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))\}]))$
131	125 127 129 130	syl12anc	$⊢ φ \to (H (card (Z)) = H (card ({W (Z)}^{-1} [\{H (card (Z))\}])) \leftrightarrow card (Z) = card ({W (Z)}^{-1} [\{H (card (Z))\}]))$
132	123 131	mpbid	$⊢ φ \to card (Z) = card ({W (Z)}^{-1} [\{H (card (Z))\}])$
133	132	eqcomd	$⊢ φ \to card ({W (Z)}^{-1} [\{H (card (Z))\}]) = card (Z)$
134		finnum	$⊢ {W (Z)}^{-1} [\{H (card (Z))\}] \in Fin \to {W (Z)}^{-1} [\{H (card (Z))\}] \in dom card$
135	119 134	syl	$⊢ φ \to {W (Z)}^{-1} [\{H (card (Z))\}] \in dom card$
136		finnum	$⊢ Z \in Fin \to Z \in dom card$
137	105 136	syl	$⊢ φ \to Z \in dom card$
138		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)$
139	135 137 138	syl2anc	$⊢ φ \to (card ({W (Z)}^{-1} [\{H (card (Z))\}]) = card (Z) \leftrightarrow {W (Z)}^{-1} [\{H (card (Z))\}] \approx Z)$
140	133 139	mpbid	$⊢ φ \to {W (Z)}^{-1} [\{H (card (Z))\}] \approx Z$
141		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)$
142	141	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)$
143	118 142	syl	$⊢ φ \to ({W (Z)}^{-1} [\{H (card (Z))\}] \subset Z \leftrightarrow \neg {W (Z)}^{-1} [\{H (card (Z))\}] = Z)$
144		php3	$⊢ (Z \in Fin \land {W (Z)}^{-1} [\{H (card (Z))\}] \subset Z) \to {W (Z)}^{-1} [\{H (card (Z))\}] ≺ Z$
145		sdomnen	$⊢ {W (Z)}^{-1} [\{H (card (Z))\}] ≺ Z \to \neg {W (Z)}^{-1} [\{H (card (Z))\}] \approx Z$
146	144 145	syl	$⊢ (Z \in Fin \land {W (Z)}^{-1} [\{H (card (Z))\}] \subset Z) \to \neg {W (Z)}^{-1} [\{H (card (Z))\}] \approx Z$
147	146	ex	$⊢ Z \in Fin \to ({W (Z)}^{-1} [\{H (card (Z))\}] \subset Z \to \neg {W (Z)}^{-1} [\{H (card (Z))\}] \approx Z)$
148	105 147	syl	$⊢ φ \to ({W (Z)}^{-1} [\{H (card (Z))\}] \subset Z \to \neg {W (Z)}^{-1} [\{H (card (Z))\}] \approx Z)$
149	143 148	sylbird	$⊢ φ \to (\neg {W (Z)}^{-1} [\{H (card (Z))\}] = Z \to \neg {W (Z)}^{-1} [\{H (card (Z))\}] \approx Z)$
150	140 149	mt4d	$⊢ φ \to {W (Z)}^{-1} [\{H (card (Z))\}] = Z$
151	109 150	eleqtrrd	$⊢ φ \to H (card (Z)) \in {W (Z)}^{-1} [\{H (card (Z))\}]$
152		fvex	$⊢ H (card (Z)) \in V$
153	152	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)))$
154	152 153	ax-mp	$⊢ H (card (Z)) \in {W (Z)}^{-1} [\{H (card (Z))\}] \leftrightarrow H (card (Z)) W (Z) H (card (Z))$
155	151 154	sylib	$⊢ φ \to H (card (Z)) W (Z) H (card (Z))$
156	25	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)$
157	156	simpld	$⊢ φ \to W (Z) We Z$
158		weso	$⊢ W (Z) We Z \to W (Z) Or Z$
159	157 158	syl	$⊢ φ \to W (Z) Or Z$
160		sonr	$⊢ (W (Z) Or Z \land H (card (Z)) \in Z) \to \neg H (card (Z)) W (Z) H (card (Z))$
161	159 109 160	syl2anc	$⊢ φ \to \neg H (card (Z)) W (Z) H (card (Z))$
162	155 161	pm2.65i	$⊢ \neg φ$

Metamath Proof Explorer

Theorem pwfseqlem4

Proof