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		f1oeq1	$⊢ N (b) = N (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	43 44	syl	$⊢ 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)$
46		xpeq12	$⊢ (b = dom O \land b = dom O) \to b \times b = dom O \times dom O$
47	46	anidms	$⊢ b = dom O \to b \times b = dom O \times dom O$
48	47	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)$
49		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)$
50	45 48 49	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)$
51	42 50	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))$
52	5	adantr	$⊢ (φ \land ψ) \to \forall b \in har (𝒫 A) (ω \subseteq b \to N (b) : b \times b \underset{1-1 onto}{⟶} b)$
53	32	a1i	$⊢ (φ \land ψ) \to dom O \in On$
54	1	adantr	$⊢ (φ \land ψ) \to G : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n})$
55		omex	$⊢ ω \in V$
56		ovex	$⊢ A^{n} \in V$
57	55 56	iunex	$⊢ ⋃_{n \in ω} (A^{n}) \in V$
58		f1dmex	$⊢ (G : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n}) \land ⋃_{n \in ω} (A^{n}) \in V) \to 𝒫 A \in V$
59	54 57 58	sylancl	$⊢ (φ \land ψ) \to 𝒫 A \in V$
60		pwexb	$⊢ A \in V \leftrightarrow 𝒫 A \in V$
61	59 60	sylibr	$⊢ (φ \land ψ) \to A \in V$
62		simprl1	$⊢ (φ \land ((t \subseteq A \land r \subseteq t \times t \land r We t) \land ω ≼ t)) \to t \subseteq A$
63	4 62	sylan2b	$⊢ (φ \land ψ) \to t \subseteq A$
64		ssdomg	$⊢ A \in V \to (t \subseteq A \to t ≼ A)$
65	61 63 64	sylc	$⊢ (φ \land ψ) \to t ≼ A$
66		canth2g	$⊢ A \in V \to A ≺ 𝒫 A$
67		sdomdom	$⊢ A ≺ 𝒫 A \to A ≼ 𝒫 A$
68	61 66 67	3syl	$⊢ (φ \land ψ) \to A ≼ 𝒫 A$
69		domtr	$⊢ (t ≼ A \land A ≼ 𝒫 A) \to t ≼ 𝒫 A$
70	65 68 69	syl2anc	$⊢ (φ \land ψ) \to t ≼ 𝒫 A$
71		endomtr	$⊢ (dom O \approx t \land t ≼ 𝒫 A) \to dom O ≼ 𝒫 A$
72	24 70 71	syl2anc	$⊢ (φ \land ψ) \to dom O ≼ 𝒫 A$
73		elharval	$⊢ dom O \in har (𝒫 A) \leftrightarrow (dom O \in On \land dom O ≼ 𝒫 A)$
74	53 72 73	sylanbrc	$⊢ (φ \land ψ) \to dom O \in har (𝒫 A)$
75	51 52 74	rspcdva	$⊢ (φ \land ψ) \to (ω \subseteq dom O \to N (dom O) : dom O \times dom O \underset{1-1 onto}{⟶} dom O)$
76	41 75	mpd	$⊢ (φ \land ψ) \to N (dom O) : dom O \times dom O \underset{1-1 onto}{⟶} dom O$
77		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$
78	19 76 77	syl2anc	$⊢ (φ \land ψ) \to (O \circ N (dom O)) : dom O \times dom O \underset{1-1 onto}{⟶} t$
79		f1of	$⊢ O : dom O \underset{1-1 onto}{⟶} t \to O : dom O ⟶ t$
80	19 79	syl	$⊢ (φ \land ψ) \to O : dom O ⟶ t$
81	80	feqmptd	$⊢ (φ \land ψ) \to O = (u \in dom O ⟼ O (u))$
82		f1oeq1	$⊢ O = (u \in dom O ⟼ O (u)) \to (O : dom O \underset{1-1 onto}{⟶} t \leftrightarrow (u \in dom O ⟼ O (u)) : dom O \underset{1-1 onto}{⟶} t)$
83	81 82	syl	$⊢ (φ \land ψ) \to (O : dom O \underset{1-1 onto}{⟶} t \leftrightarrow (u \in dom O ⟼ O (u)) : dom O \underset{1-1 onto}{⟶} t)$
84	19 83	mpbid	$⊢ (φ \land ψ) \to (u \in dom O ⟼ O (u)) : dom O \underset{1-1 onto}{⟶} t$
85	80	feqmptd	$⊢ (φ \land ψ) \to O = (v \in dom O ⟼ O (v))$
86		f1oeq1	$⊢ O = (v \in dom O ⟼ O (v)) \to (O : dom O \underset{1-1 onto}{⟶} t \leftrightarrow (v \in dom O ⟼ O (v)) : dom O \underset{1-1 onto}{⟶} t)$
87	85 86	syl	$⊢ (φ \land ψ) \to (O : dom O \underset{1-1 onto}{⟶} t \leftrightarrow (v \in dom O ⟼ O (v)) : dom O \underset{1-1 onto}{⟶} t)$
88	19 87	mpbid	$⊢ (φ \land ψ) \to (v \in dom O ⟼ O (v)) : dom O \underset{1-1 onto}{⟶} t$
89	84 88	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$
90		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)$
91	7 90	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$
92	89 91	sylibr	$⊢ (φ \land ψ) \to T : dom O \times dom O \underset{1-1 onto}{⟶} t \times t$
93		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$
94	92 93	syl	$⊢ (φ \land ψ) \to T^{-1} : t \times t \underset{1-1 onto}{⟶} dom O \times dom O$
95		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$
96	78 94 95	syl2anc	$⊢ (φ \land ψ) \to ((O \circ N (dom O)) \circ T^{-1}) : t \times t \underset{1-1 onto}{⟶} t$
97		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)$
98	8 97	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$
99	96 98	sylibr	$⊢ (φ \land ψ) \to P : t \times t \underset{1-1 onto}{⟶} t$
100		f1of1	$⊢ P : t \times t \underset{1-1 onto}{⟶} t \to P : t \times t \underset{1-1}{⟶} t$
101	99 100	syl	$⊢ (φ \land ψ) \to P : t \times t \underset{1-1}{⟶} t$
102		f1of1	$⊢ O : dom O \underset{1-1 onto}{⟶} t \to O : dom O \underset{1-1}{⟶} t$
103	19 102	syl	$⊢ (φ \land ψ) \to O : dom O \underset{1-1}{⟶} t$
104		f1ssres	$⊢ (O : dom O \underset{1-1}{⟶} t \land ω \subseteq dom O) \to ({O ↾}_{ω}) : ω \underset{1-1}{⟶} t$
105	103 41 104	syl2anc	$⊢ (φ \land ψ) \to ({O ↾}_{ω}) : ω \underset{1-1}{⟶} t$
106		f1f1orn	$⊢ ({O ↾}_{ω}) : ω \underset{1-1}{⟶} t \to ({O ↾}_{ω}) : ω \underset{1-1 onto}{⟶} ran ({O ↾}_{ω})$
107	105 106	syl	$⊢ (φ \land ψ) \to ({O ↾}_{ω}) : ω \underset{1-1 onto}{⟶} ran ({O ↾}_{ω})$
108	80 41	feqresmpt	$⊢ (φ \land ψ) \to {O ↾}_{ω} = (x \in ω ⟼ O (x))$
109		f1oeq1	$⊢ {O ↾}_{ω} = (x \in ω ⟼ O (x)) \to (({O ↾}_{ω}) : ω \underset{1-1 onto}{⟶} ran ({O ↾}_{ω}) \leftrightarrow (x \in ω ⟼ O (x)) : ω \underset{1-1 onto}{⟶} ran ({O ↾}_{ω}))$
110	108 109	syl	$⊢ (φ \land ψ) \to (({O ↾}_{ω}) : ω \underset{1-1 onto}{⟶} ran ({O ↾}_{ω}) \leftrightarrow (x \in ω ⟼ O (x)) : ω \underset{1-1 onto}{⟶} ran ({O ↾}_{ω}))$
111	107 110	mpbid	$⊢ (φ \land ψ) \to (x \in ω ⟼ O (x)) : ω \underset{1-1 onto}{⟶} ran ({O ↾}_{ω})$
112		mptresid	$⊢ {I ↾}_{t} = (y \in t ⟼ y)$
113	112	eqcomi	$⊢ (y \in t ⟼ y) = {I ↾}_{t}$
114		f1oi	$⊢ ({I ↾}_{t}) : t \underset{1-1 onto}{⟶} t$
115		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)$
116	114 115	mpbiri	$⊢ (y \in t ⟼ y) = {I ↾}_{t} \to (y \in t ⟼ y) : t \underset{1-1 onto}{⟶} t$
117	113 116	mp1i	$⊢ (φ \land ψ) \to (y \in t ⟼ y) : t \underset{1-1 onto}{⟶} t$
118	111 117	xpf1o	$⊢ (φ \land ψ) \to (x \in ω, y \in t ⟼ ⟨O (x), y⟩) : ω \times t \underset{1-1 onto}{⟶} ran ({O ↾}_{ω}) \times t$
119		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)$
120	11 119	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$
121	118 120	sylibr	$⊢ (φ \land ψ) \to I : ω \times t \underset{1-1 onto}{⟶} ran ({O ↾}_{ω}) \times t$
122		f1of1	$⊢ I : ω \times t \underset{1-1 onto}{⟶} ran ({O ↾}_{ω}) \times t \to I : ω \times t \underset{1-1}{⟶} ran ({O ↾}_{ω}) \times t$
123	121 122	syl	$⊢ (φ \land ψ) \to I : ω \times t \underset{1-1}{⟶} ran ({O ↾}_{ω}) \times t$
124		f1f	$⊢ ({O ↾}_{ω}) : ω \underset{1-1}{⟶} t \to ({O ↾}_{ω}) : ω ⟶ t$
125		frn	$⊢ ({O ↾}_{ω}) : ω ⟶ t \to ran ({O ↾}_{ω}) \subseteq t$
126		xpss1	$⊢ ran ({O ↾}_{ω}) \subseteq t \to ran ({O ↾}_{ω}) \times t \subseteq t \times t$
127	105 124 125 126	4syl	$⊢ (φ \land ψ) \to ran ({O ↾}_{ω}) \times t \subseteq t \times t$
128		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$
129	123 127 128	syl2anc	$⊢ (φ \land ψ) \to I : ω \times t \underset{1-1}{⟶} t \times t$
130		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$
131	101 129 130	syl2anc	$⊢ (φ \land ψ) \to (P \circ I) : ω \times t \underset{1-1}{⟶} t$
132	13	a1i	$⊢ (φ \land ψ) \to t \in V$
133		peano1	$⊢ \emptyset \in ω$
134	133	a1i	$⊢ (φ \land ψ) \to \emptyset \in ω$
135	41 134	sseldd	$⊢ (φ \land ψ) \to \emptyset \in dom O$
136	80 135	ffvelrnd	$⊢ (φ \land ψ) \to O (\emptyset) \in t$
137	132 136 99 9 10	fseqenlem2	$⊢ (φ \land ψ) \to Q : ⋃_{n \in ω} (t^{n}) \underset{1-1}{⟶} ω \times t$
138		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$
139	131 137 138	syl2anc	$⊢ (φ \land ψ) \to ((P \circ I) \circ Q) : ⋃_{n \in ω} (t^{n}) \underset{1-1}{⟶} t$
140		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)$
141	12 140	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$
142	139 141	sylibr	$⊢ (φ \land ψ) \to K : ⋃_{n \in ω} (t^{n}) \underset{1-1}{⟶} t$
143		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)))\})$
144		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\})))$
145		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))\}$
146	145	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))\}$
147		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))\}$
148	1 2 3 4 142 143 144 146 147	pwfseqlem4	$⊢ \neg φ$

Metamath Proof Explorer

Theorem pwfseqlem5

Proof