pwfseqlem5

Description: Lemma for pwfseq . Although in some ways pwfseqlem4 is the "main" part of the proof, one last aspect which makes up a remark in the original text is by far the hardest part to formalize. The main proof relies on the existence of an injection K from the set of finite sequences on an infinite set x to x . Now this alone would not be difficult to prove; this is mostly the claim of fseqen . However, what is needed for the proof is acanonical injection on these sets, so we have to start from scratch pulling together explicit bijections from the lemmas.

If one attempts such a program, it will mostly go through, but there is one key step which is inherently nonconstructive, namely the proof of infxpen . The resolution is not obvious, but it turns out that reversing an infinite ordinal's Cantor normal form absorbs all the non-leading terms ( cnfcom3c ), which can be used to construct a pairing function explicitly using properties of the ordinal exponential ( infxpenc ). (Contributed by Mario Carneiro, 31-May-2015)

	Ref	Expression
Hypotheses	pwfseqlem5.g	$⊢ φ \to G : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n})$
	pwfseqlem5.x	$⊢ φ \to X \subseteq A$
	pwfseqlem5.h	$⊢ φ \to H : ω \underset{1-1 onto}{⟶} X$
	pwfseqlem5.ps	$⊢ ψ \leftrightarrow ((t \subseteq A \land r \subseteq t \times t \land r We t) \land ω ≼ t)$
	pwfseqlem5.n	$⊢ φ \to \forall b \in har (𝒫 A) (ω \subseteq b \to N (b) : b \times b \underset{1-1 onto}{⟶} b)$
	pwfseqlem5.o	$⊢ O = OrdIso (r, t)$
	pwfseqlem5.t	$⊢ T = (u \in dom O, v \in dom O ⟼ ⟨O (u), O (v)⟩)$
	pwfseqlem5.p	$⊢ P = (O \circ N (dom O)) \circ T^{-1}$
	pwfseqlem5.s	$⊢ S = {seq}_{ω} ((k \in V, f \in V ⟼ (x \in (t^{suc k}) ⟼ f ({x ↾}_{k}) P x (k))), \{⟨\emptyset, O (\emptyset)⟩\})$
	pwfseqlem5.q	$⊢ Q = (y \in ⋃_{n \in ω} (t^{n}) ⟼ ⟨dom y, S (dom y) (y)⟩)$
	pwfseqlem5.i	$⊢ I = (x \in ω, y \in t ⟼ ⟨O (x), y⟩)$
	pwfseqlem5.k	$⊢ K = (P \circ I) \circ Q$
Assertion	pwfseqlem5	$⊢ \neg φ$

Proof

Step	Hyp	Ref	Expression
1		pwfseqlem5.g	$⊢ φ \to G : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n})$
2		pwfseqlem5.x	$⊢ φ \to X \subseteq A$
3		pwfseqlem5.h	$⊢ φ \to H : ω \underset{1-1 onto}{⟶} X$
4		pwfseqlem5.ps	$⊢ ψ \leftrightarrow ((t \subseteq A \land r \subseteq t \times t \land r We t) \land ω ≼ t)$
5		pwfseqlem5.n	$⊢ φ \to \forall b \in har (𝒫 A) (ω \subseteq b \to N (b) : b \times b \underset{1-1 onto}{⟶} b)$
6		pwfseqlem5.o	$⊢ O = OrdIso (r, t)$
7		pwfseqlem5.t	$⊢ T = (u \in dom O, v \in dom O ⟼ ⟨O (u), O (v)⟩)$
8		pwfseqlem5.p	$⊢ P = (O \circ N (dom O)) \circ T^{-1}$
9		pwfseqlem5.s	$⊢ S = {seq}_{ω} ((k \in V, f \in V ⟼ (x \in (t^{suc k}) ⟼ f ({x ↾}_{k}) P x (k))), \{⟨\emptyset, O (\emptyset)⟩\})$
10		pwfseqlem5.q	$⊢ Q = (y \in ⋃_{n \in ω} (t^{n}) ⟼ ⟨dom y, S (dom y) (y)⟩)$
11		pwfseqlem5.i	$⊢ I = (x \in ω, y \in t ⟼ ⟨O (x), y⟩)$
12		pwfseqlem5.k	$⊢ K = (P \circ I) \circ Q$
13		vex	$⊢ t \in V$
14		simprl3	$⊢ (φ \land ((t \subseteq A \land r \subseteq t \times t \land r We t) \land ω ≼ t)) \to r We t$
15	4 14	sylan2b	$⊢ (φ \land ψ) \to r We t$
16	6	oiiso	$⊢ (t \in V \land r We t) \to O {Isom}_{E, r} (dom O, t)$
17	13 15 16	sylancr	$⊢ (φ \land ψ) \to O {Isom}_{E, r} (dom O, t)$
18		isof1o	$⊢ O {Isom}_{E, r} (dom O, t) \to O : dom O \underset{1-1 onto}{⟶} t$
19	17 18	syl	$⊢ (φ \land ψ) \to O : dom O \underset{1-1 onto}{⟶} t$
20		cardom	$⊢ card (ω) = ω$
21		simprr	$⊢ (φ \land ((t \subseteq A \land r \subseteq t \times t \land r We t) \land ω ≼ t)) \to ω ≼ t$
22	4 21	sylan2b	$⊢ (φ \land ψ) \to ω ≼ t$
23	6	oien	$⊢ (t \in V \land r We t) \to dom O \approx t$
24	13 15 23	sylancr	$⊢ (φ \land ψ) \to dom O \approx t$
25	24	ensymd	$⊢ (φ \land ψ) \to t \approx dom O$
26		domentr	$⊢ (ω ≼ t \land t \approx dom O) \to ω ≼ dom O$
27	22 25 26	syl2anc	$⊢ (φ \land ψ) \to ω ≼ dom O$
28		omelon	$⊢ ω \in On$
29		onenon	$⊢ ω \in On \to ω \in dom card$
30	28 29	ax-mp	$⊢ ω \in dom card$
31	6	oion	$⊢ t \in V \to dom O \in On$
32	31	elv	$⊢ dom O \in On$
33		onenon	$⊢ dom O \in On \to dom O \in dom card$
34	32 33	mp1i	$⊢ (φ \land ψ) \to dom O \in dom card$
35		carddom2	$⊢ (ω \in dom card \land dom O \in dom card) \to (card (ω) \subseteq card (dom O) \leftrightarrow ω ≼ dom O)$
36	30 34 35	sylancr	$⊢ (φ \land ψ) \to (card (ω) \subseteq card (dom O) \leftrightarrow ω ≼ dom O)$
37	27 36	mpbird	$⊢ (φ \land ψ) \to card (ω) \subseteq card (dom O)$
38	20 37	eqsstrrid	$⊢ (φ \land ψ) \to ω \subseteq card (dom O)$
39		cardonle	$⊢ dom O \in On \to card (dom O) \subseteq dom O$
40	32 39	mp1i	$⊢ (φ \land ψ) \to card (dom O) \subseteq dom O$
41	38 40	sstrd	$⊢ (φ \land ψ) \to ω \subseteq dom O$
42		sseq2	$⊢ b = dom O \to (ω \subseteq b \leftrightarrow ω \subseteq dom O)$
43		fveq2	$⊢ b = dom O \to N (b) = N (dom O)$
44	43	f1oeq1d	$⊢ b = dom O \to (N (b) : b \times b \underset{1-1 onto}{⟶} b \leftrightarrow N (dom O) : b \times b \underset{1-1 onto}{⟶} b)$
45		xpeq12	$⊢ (b = dom O \land b = dom O) \to b \times b = dom O \times dom O$
46	45	anidms	$⊢ b = dom O \to b \times b = dom O \times dom O$
47	46	f1oeq2d	$⊢ b = dom O \to (N (dom O) : b \times b \underset{1-1 onto}{⟶} b \leftrightarrow N (dom O) : dom O \times dom O \underset{1-1 onto}{⟶} b)$
48		f1oeq3	$⊢ b = dom O \to (N (dom O) : dom O \times dom O \underset{1-1 onto}{⟶} b \leftrightarrow N (dom O) : dom O \times dom O \underset{1-1 onto}{⟶} dom O)$
49	44 47 48	3bitrd	$⊢ b = dom O \to (N (b) : b \times b \underset{1-1 onto}{⟶} b \leftrightarrow N (dom O) : dom O \times dom O \underset{1-1 onto}{⟶} dom O)$
50	42 49	imbi12d	$⊢ b = dom O \to ((ω \subseteq b \to N (b) : b \times b \underset{1-1 onto}{⟶} b) \leftrightarrow (ω \subseteq dom O \to N (dom O) : dom O \times dom O \underset{1-1 onto}{⟶} dom O))$
51	5	adantr	$⊢ (φ \land ψ) \to \forall b \in har (𝒫 A) (ω \subseteq b \to N (b) : b \times b \underset{1-1 onto}{⟶} b)$
52	32	a1i	$⊢ (φ \land ψ) \to dom O \in On$
53	1	adantr	$⊢ (φ \land ψ) \to G : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n})$
54		omex	$⊢ ω \in V$
55		ovex	$⊢ A^{n} \in V$
56	54 55	iunex	$⊢ ⋃_{n \in ω} (A^{n}) \in V$
57		f1dmex	$⊢ (G : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n}) \land ⋃_{n \in ω} (A^{n}) \in V) \to 𝒫 A \in V$
58	53 56 57	sylancl	$⊢ (φ \land ψ) \to 𝒫 A \in V$
59		pwexb	$⊢ A \in V \leftrightarrow 𝒫 A \in V$
60	58 59	sylibr	$⊢ (φ \land ψ) \to A \in V$
61		simprl1	$⊢ (φ \land ((t \subseteq A \land r \subseteq t \times t \land r We t) \land ω ≼ t)) \to t \subseteq A$
62	4 61	sylan2b	$⊢ (φ \land ψ) \to t \subseteq A$
63		ssdomg	$⊢ A \in V \to (t \subseteq A \to t ≼ A)$
64	60 62 63	sylc	$⊢ (φ \land ψ) \to t ≼ A$
65		canth2g	$⊢ A \in V \to A ≺ 𝒫 A$
66		sdomdom	$⊢ A ≺ 𝒫 A \to A ≼ 𝒫 A$
67	60 65 66	3syl	$⊢ (φ \land ψ) \to A ≼ 𝒫 A$
68		domtr	$⊢ (t ≼ A \land A ≼ 𝒫 A) \to t ≼ 𝒫 A$
69	64 67 68	syl2anc	$⊢ (φ \land ψ) \to t ≼ 𝒫 A$
70		endomtr	$⊢ (dom O \approx t \land t ≼ 𝒫 A) \to dom O ≼ 𝒫 A$
71	24 69 70	syl2anc	$⊢ (φ \land ψ) \to dom O ≼ 𝒫 A$
72		elharval	$⊢ dom O \in har (𝒫 A) \leftrightarrow (dom O \in On \land dom O ≼ 𝒫 A)$
73	52 71 72	sylanbrc	$⊢ (φ \land ψ) \to dom O \in har (𝒫 A)$
74	50 51 73	rspcdva	$⊢ (φ \land ψ) \to (ω \subseteq dom O \to N (dom O) : dom O \times dom O \underset{1-1 onto}{⟶} dom O)$
75	41 74	mpd	$⊢ (φ \land ψ) \to N (dom O) : dom O \times dom O \underset{1-1 onto}{⟶} dom O$
76		f1oco	$⊢ (O : dom O \underset{1-1 onto}{⟶} t \land N (dom O) : dom O \times dom O \underset{1-1 onto}{⟶} dom O) \to (O \circ N (dom O)) : dom O \times dom O \underset{1-1 onto}{⟶} t$
77	19 75 76	syl2anc	$⊢ (φ \land ψ) \to (O \circ N (dom O)) : dom O \times dom O \underset{1-1 onto}{⟶} t$
78		f1of	$⊢ O : dom O \underset{1-1 onto}{⟶} t \to O : dom O ⟶ t$
79	19 78	syl	$⊢ (φ \land ψ) \to O : dom O ⟶ t$
80	79	feqmptd	$⊢ (φ \land ψ) \to O = (u \in dom O ⟼ O (u))$
81	80	f1oeq1d	$⊢ (φ \land ψ) \to (O : dom O \underset{1-1 onto}{⟶} t \leftrightarrow (u \in dom O ⟼ O (u)) : dom O \underset{1-1 onto}{⟶} t)$
82	19 81	mpbid	$⊢ (φ \land ψ) \to (u \in dom O ⟼ O (u)) : dom O \underset{1-1 onto}{⟶} t$
83	79	feqmptd	$⊢ (φ \land ψ) \to O = (v \in dom O ⟼ O (v))$
84	83	f1oeq1d	$⊢ (φ \land ψ) \to (O : dom O \underset{1-1 onto}{⟶} t \leftrightarrow (v \in dom O ⟼ O (v)) : dom O \underset{1-1 onto}{⟶} t)$
85	19 84	mpbid	$⊢ (φ \land ψ) \to (v \in dom O ⟼ O (v)) : dom O \underset{1-1 onto}{⟶} t$
86	82 85	xpf1o	$⊢ (φ \land ψ) \to (u \in dom O, v \in dom O ⟼ ⟨O (u), O (v)⟩) : dom O \times dom O \underset{1-1 onto}{⟶} t \times t$
87		f1oeq1	$⊢ T = (u \in dom O, v \in dom O ⟼ ⟨O (u), O (v)⟩) \to (T : dom O \times dom O \underset{1-1 onto}{⟶} t \times t \leftrightarrow (u \in dom O, v \in dom O ⟼ ⟨O (u), O (v)⟩) : dom O \times dom O \underset{1-1 onto}{⟶} t \times t)$
88	7 87	ax-mp	$⊢ T : dom O \times dom O \underset{1-1 onto}{⟶} t \times t \leftrightarrow (u \in dom O, v \in dom O ⟼ ⟨O (u), O (v)⟩) : dom O \times dom O \underset{1-1 onto}{⟶} t \times t$
89	86 88	sylibr	$⊢ (φ \land ψ) \to T : dom O \times dom O \underset{1-1 onto}{⟶} t \times t$
90		f1ocnv	$⊢ T : dom O \times dom O \underset{1-1 onto}{⟶} t \times t \to T^{-1} : t \times t \underset{1-1 onto}{⟶} dom O \times dom O$
91	89 90	syl	$⊢ (φ \land ψ) \to T^{-1} : t \times t \underset{1-1 onto}{⟶} dom O \times dom O$
92		f1oco	$⊢ ((O \circ N (dom O)) : dom O \times dom O \underset{1-1 onto}{⟶} t \land T^{-1} : t \times t \underset{1-1 onto}{⟶} dom O \times dom O) \to ((O \circ N (dom O)) \circ T^{-1}) : t \times t \underset{1-1 onto}{⟶} t$
93	77 91 92	syl2anc	$⊢ (φ \land ψ) \to ((O \circ N (dom O)) \circ T^{-1}) : t \times t \underset{1-1 onto}{⟶} t$
94		f1oeq1	$⊢ P = (O \circ N (dom O)) \circ T^{-1} \to (P : t \times t \underset{1-1 onto}{⟶} t \leftrightarrow ((O \circ N (dom O)) \circ T^{-1}) : t \times t \underset{1-1 onto}{⟶} t)$
95	8 94	ax-mp	$⊢ P : t \times t \underset{1-1 onto}{⟶} t \leftrightarrow ((O \circ N (dom O)) \circ T^{-1}) : t \times t \underset{1-1 onto}{⟶} t$
96	93 95	sylibr	$⊢ (φ \land ψ) \to P : t \times t \underset{1-1 onto}{⟶} t$
97		f1of1	$⊢ P : t \times t \underset{1-1 onto}{⟶} t \to P : t \times t \underset{1-1}{⟶} t$
98	96 97	syl	$⊢ (φ \land ψ) \to P : t \times t \underset{1-1}{⟶} t$
99		f1of1	$⊢ O : dom O \underset{1-1 onto}{⟶} t \to O : dom O \underset{1-1}{⟶} t$
100	19 99	syl	$⊢ (φ \land ψ) \to O : dom O \underset{1-1}{⟶} t$
101		f1ssres	$⊢ (O : dom O \underset{1-1}{⟶} t \land ω \subseteq dom O) \to ({O ↾}_{ω}) : ω \underset{1-1}{⟶} t$
102	100 41 101	syl2anc	$⊢ (φ \land ψ) \to ({O ↾}_{ω}) : ω \underset{1-1}{⟶} t$
103		f1f1orn	$⊢ ({O ↾}_{ω}) : ω \underset{1-1}{⟶} t \to ({O ↾}_{ω}) : ω \underset{1-1 onto}{⟶} ran ({O ↾}_{ω})$
104	102 103	syl	$⊢ (φ \land ψ) \to ({O ↾}_{ω}) : ω \underset{1-1 onto}{⟶} ran ({O ↾}_{ω})$
105	79 41	feqresmpt	$⊢ (φ \land ψ) \to {O ↾}_{ω} = (x \in ω ⟼ O (x))$
106	105	f1oeq1d	$⊢ (φ \land ψ) \to (({O ↾}_{ω}) : ω \underset{1-1 onto}{⟶} ran ({O ↾}_{ω}) \leftrightarrow (x \in ω ⟼ O (x)) : ω \underset{1-1 onto}{⟶} ran ({O ↾}_{ω}))$
107	104 106	mpbid	$⊢ (φ \land ψ) \to (x \in ω ⟼ O (x)) : ω \underset{1-1 onto}{⟶} ran ({O ↾}_{ω})$
108		mptresid	$⊢ {I ↾}_{t} = (y \in t ⟼ y)$
109	108	eqcomi	$⊢ (y \in t ⟼ y) = {I ↾}_{t}$
110		f1oi	$⊢ ({I ↾}_{t}) : t \underset{1-1 onto}{⟶} t$
111		f1oeq1	$⊢ (y \in t ⟼ y) = {I ↾}_{t} \to ((y \in t ⟼ y) : t \underset{1-1 onto}{⟶} t \leftrightarrow ({I ↾}_{t}) : t \underset{1-1 onto}{⟶} t)$
112	110 111	mpbiri	$⊢ (y \in t ⟼ y) = {I ↾}_{t} \to (y \in t ⟼ y) : t \underset{1-1 onto}{⟶} t$
113	109 112	mp1i	$⊢ (φ \land ψ) \to (y \in t ⟼ y) : t \underset{1-1 onto}{⟶} t$
114	107 113	xpf1o	$⊢ (φ \land ψ) \to (x \in ω, y \in t ⟼ ⟨O (x), y⟩) : ω \times t \underset{1-1 onto}{⟶} ran ({O ↾}_{ω}) \times t$
115		f1oeq1	$⊢ I = (x \in ω, y \in t ⟼ ⟨O (x), y⟩) \to (I : ω \times t \underset{1-1 onto}{⟶} ran ({O ↾}_{ω}) \times t \leftrightarrow (x \in ω, y \in t ⟼ ⟨O (x), y⟩) : ω \times t \underset{1-1 onto}{⟶} ran ({O ↾}_{ω}) \times t)$
116	11 115	ax-mp	$⊢ I : ω \times t \underset{1-1 onto}{⟶} ran ({O ↾}_{ω}) \times t \leftrightarrow (x \in ω, y \in t ⟼ ⟨O (x), y⟩) : ω \times t \underset{1-1 onto}{⟶} ran ({O ↾}_{ω}) \times t$
117	114 116	sylibr	$⊢ (φ \land ψ) \to I : ω \times t \underset{1-1 onto}{⟶} ran ({O ↾}_{ω}) \times t$
118		f1of1	$⊢ I : ω \times t \underset{1-1 onto}{⟶} ran ({O ↾}_{ω}) \times t \to I : ω \times t \underset{1-1}{⟶} ran ({O ↾}_{ω}) \times t$
119	117 118	syl	$⊢ (φ \land ψ) \to I : ω \times t \underset{1-1}{⟶} ran ({O ↾}_{ω}) \times t$
120		f1f	$⊢ ({O ↾}_{ω}) : ω \underset{1-1}{⟶} t \to ({O ↾}_{ω}) : ω ⟶ t$
121		frn	$⊢ ({O ↾}_{ω}) : ω ⟶ t \to ran ({O ↾}_{ω}) \subseteq t$
122		xpss1	$⊢ ran ({O ↾}_{ω}) \subseteq t \to ran ({O ↾}_{ω}) \times t \subseteq t \times t$
123	102 120 121 122	4syl	$⊢ (φ \land ψ) \to ran ({O ↾}_{ω}) \times t \subseteq t \times t$
124		f1ss	$⊢ (I : ω \times t \underset{1-1}{⟶} ran ({O ↾}_{ω}) \times t \land ran ({O ↾}_{ω}) \times t \subseteq t \times t) \to I : ω \times t \underset{1-1}{⟶} t \times t$
125	119 123 124	syl2anc	$⊢ (φ \land ψ) \to I : ω \times t \underset{1-1}{⟶} t \times t$
126		f1co	$⊢ (P : t \times t \underset{1-1}{⟶} t \land I : ω \times t \underset{1-1}{⟶} t \times t) \to (P \circ I) : ω \times t \underset{1-1}{⟶} t$
127	98 125 126	syl2anc	$⊢ (φ \land ψ) \to (P \circ I) : ω \times t \underset{1-1}{⟶} t$
128	13	a1i	$⊢ (φ \land ψ) \to t \in V$
129		peano1	$⊢ \emptyset \in ω$
130	129	a1i	$⊢ (φ \land ψ) \to \emptyset \in ω$
131	41 130	sseldd	$⊢ (φ \land ψ) \to \emptyset \in dom O$
132	79 131	ffvelrnd	$⊢ (φ \land ψ) \to O (\emptyset) \in t$
133	128 132 96 9 10	fseqenlem2	$⊢ (φ \land ψ) \to Q : ⋃_{n \in ω} (t^{n}) \underset{1-1}{⟶} ω \times t$
134		f1co	$⊢ ((P \circ I) : ω \times t \underset{1-1}{⟶} t \land Q : ⋃_{n \in ω} (t^{n}) \underset{1-1}{⟶} ω \times t) \to ((P \circ I) \circ Q) : ⋃_{n \in ω} (t^{n}) \underset{1-1}{⟶} t$
135	127 133 134	syl2anc	$⊢ (φ \land ψ) \to ((P \circ I) \circ Q) : ⋃_{n \in ω} (t^{n}) \underset{1-1}{⟶} t$
136		f1eq1	$⊢ K = (P \circ I) \circ Q \to (K : ⋃_{n \in ω} (t^{n}) \underset{1-1}{⟶} t \leftrightarrow ((P \circ I) \circ Q) : ⋃_{n \in ω} (t^{n}) \underset{1-1}{⟶} t)$
137	12 136	ax-mp	$⊢ K : ⋃_{n \in ω} (t^{n}) \underset{1-1}{⟶} t \leftrightarrow ((P \circ I) \circ Q) : ⋃_{n \in ω} (t^{n}) \underset{1-1}{⟶} t$
138	135 137	sylibr	$⊢ (φ \land ψ) \to K : ⋃_{n \in ω} (t^{n}) \underset{1-1}{⟶} t$
139		eqid	$⊢ G (\{i \in t \| (K^{-1} (i) \in ran G \land \neg i \in G^{-1} (K^{-1} (i)))\}) = G (\{i \in t \| (K^{-1} (i) \in ran G \land \neg i \in G^{-1} (K^{-1} (i)))\})$
140		eqid	$⊢ (t \in V, r \in V ⟼ if (t \in Fin, H (card (t)), G (\{i \in t \| (K^{-1} (i) \in ran G \land \neg i \in G^{-1} (K^{-1} (i)))\}) (⋂ \{z \in ω \| \neg G (\{i \in t \| (K^{-1} (i) \in ran G \land \neg i \in G^{-1} (K^{-1} (i)))\}) (z) \in t\}))) = (t \in V, r \in V ⟼ if (t \in Fin, H (card (t)), G (\{i \in t \| (K^{-1} (i) \in ran G \land \neg i \in G^{-1} (K^{-1} (i)))\}) (⋂ \{z \in ω \| \neg G (\{i \in t \| (K^{-1} (i) \in ran G \land \neg i \in G^{-1} (K^{-1} (i)))\}) (z) \in t\})))$
141		eqid	$⊢ \{⟨c, d⟩ \| ((c \subseteq A \land d \subseteq c \times c) \land (d We c \land \forall m \in c \underset{˙}{[} d^{-1} [\{m\}] / j \underset{˙}{]} j (t \in V, r \in V ⟼ if (t \in Fin, H (card (t)), G (\{i \in t \| (K^{-1} (i) \in ran G \land \neg i \in G^{-1} (K^{-1} (i)))\}) (⋂ \{z \in ω \| \neg G (\{i \in t \| (K^{-1} (i) \in ran G \land \neg i \in G^{-1} (K^{-1} (i)))\}) (z) \in t\}))) (d \cap (j \times j)) = m))\} = \{⟨c, d⟩ \| ((c \subseteq A \land d \subseteq c \times c) \land (d We c \land \forall m \in c \underset{˙}{[} d^{-1} [\{m\}] / j \underset{˙}{]} j (t \in V, r \in V ⟼ if (t \in Fin, H (card (t)), G (\{i \in t \| (K^{-1} (i) \in ran G \land \neg i \in G^{-1} (K^{-1} (i)))\}) (⋂ \{z \in ω \| \neg G (\{i \in t \| (K^{-1} (i) \in ran G \land \neg i \in G^{-1} (K^{-1} (i)))\}) (z) \in t\}))) (d \cap (j \times j)) = m))\}$
142	141	fpwwe2cbv	$⊢ \{⟨c, d⟩ \| ((c \subseteq A \land d \subseteq c \times c) \land (d We c \land \forall m \in c \underset{˙}{[} d^{-1} [\{m\}] / j \underset{˙}{]} j (t \in V, r \in V ⟼ if (t \in Fin, H (card (t)), G (\{i \in t \| (K^{-1} (i) \in ran G \land \neg i \in G^{-1} (K^{-1} (i)))\}) (⋂ \{z \in ω \| \neg G (\{i \in t \| (K^{-1} (i) \in ran G \land \neg i \in G^{-1} (K^{-1} (i)))\}) (z) \in t\}))) (d \cap (j \times j)) = m))\} = \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall b \in a \underset{˙}{[} s^{-1} [\{b\}] / w \underset{˙}{]} w (t \in V, r \in V ⟼ if (t \in Fin, H (card (t)), G (\{i \in t \| (K^{-1} (i) \in ran G \land \neg i \in G^{-1} (K^{-1} (i)))\}) (⋂ \{z \in ω \| \neg G (\{i \in t \| (K^{-1} (i) \in ran G \land \neg i \in G^{-1} (K^{-1} (i)))\}) (z) \in t\}))) (s \cap (w \times w)) = b))\}$
143		eqid	$⊢ ⋃ dom \{⟨c, d⟩ \| ((c \subseteq A \land d \subseteq c \times c) \land (d We c \land \forall m \in c \underset{˙}{[} d^{-1} [\{m\}] / j \underset{˙}{]} j (t \in V, r \in V ⟼ if (t \in Fin, H (card (t)), G (\{i \in t \| (K^{-1} (i) \in ran G \land \neg i \in G^{-1} (K^{-1} (i)))\}) (⋂ \{z \in ω \| \neg G (\{i \in t \| (K^{-1} (i) \in ran G \land \neg i \in G^{-1} (K^{-1} (i)))\}) (z) \in t\}))) (d \cap (j \times j)) = m))\} = ⋃ dom \{⟨c, d⟩ \| ((c \subseteq A \land d \subseteq c \times c) \land (d We c \land \forall m \in c \underset{˙}{[} d^{-1} [\{m\}] / j \underset{˙}{]} j (t \in V, r \in V ⟼ if (t \in Fin, H (card (t)), G (\{i \in t \| (K^{-1} (i) \in ran G \land \neg i \in G^{-1} (K^{-1} (i)))\}) (⋂ \{z \in ω \| \neg G (\{i \in t \| (K^{-1} (i) \in ran G \land \neg i \in G^{-1} (K^{-1} (i)))\}) (z) \in t\}))) (d \cap (j \times j)) = m))\}$
144	1 2 3 4 138 139 140 142 143	pwfseqlem4	$⊢ \neg φ$

Metamath Proof Explorer

Theorem pwfseqlem5

Proof