pwfseqlem3

Description: Lemma for pwfseq . Using the construction D from pwfseqlem1 , produce a function F that maps any well-ordered infinite set to an element outside the set. (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\})))$
Assertion	pwfseqlem3	$⊢ (φ \land ψ) \to x F r \in (A ∖ x)$

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		vex	$⊢ x \in V$
9		vex	$⊢ r \in V$
10		fvex	$⊢ H (card (x)) \in V$
11		fvex	$⊢ D (⋂ \{z \in ω \| \neg D (z) \in x\}) \in V$
12	10 11	ifex	$⊢ if (x \in Fin, H (card (x)), D (⋂ \{z \in ω \| \neg D (z) \in x\})) \in V$
13	7	ovmpt4g	$⊢ (x \in V \land r \in V \land if (x \in Fin, H (card (x)), D (⋂ \{z \in ω \| \neg D (z) \in x\})) \in V) \to x F r = if (x \in Fin, H (card (x)), D (⋂ \{z \in ω \| \neg D (z) \in x\}))$
14	8 9 12 13	mp3an	$⊢ x F r = if (x \in Fin, H (card (x)), D (⋂ \{z \in ω \| \neg D (z) \in x\}))$
15	4	simprbi	$⊢ ψ \to ω ≼ x$
16	15	adantl	$⊢ (φ \land ψ) \to ω ≼ x$
17		domnsym	$⊢ ω ≼ x \to \neg x ≺ ω$
18	16 17	syl	$⊢ (φ \land ψ) \to \neg x ≺ ω$
19		isfinite	$⊢ x \in Fin \leftrightarrow x ≺ ω$
20	18 19	sylnibr	$⊢ (φ \land ψ) \to \neg x \in Fin$
21	20	iffalsed	$⊢ (φ \land ψ) \to if (x \in Fin, H (card (x)), D (⋂ \{z \in ω \| \neg D (z) \in x\})) = D (⋂ \{z \in ω \| \neg D (z) \in x\})$
22	14 21	eqtrid	$⊢ (φ \land ψ) \to x F r = D (⋂ \{z \in ω \| \neg D (z) \in x\})$
23	1 2 3 4 5 6	pwfseqlem1	$⊢ (φ \land ψ) \to D \in (⋃_{n \in ω} (A^{n}) ∖ ⋃_{n \in ω} (x^{n}))$
24		eldif	$⊢ D \in (⋃_{n \in ω} (A^{n}) ∖ ⋃_{n \in ω} (x^{n})) \leftrightarrow (D \in ⋃_{n \in ω} (A^{n}) \land \neg D \in ⋃_{n \in ω} (x^{n}))$
25	23 24	sylib	$⊢ (φ \land ψ) \to (D \in ⋃_{n \in ω} (A^{n}) \land \neg D \in ⋃_{n \in ω} (x^{n}))$
26	25	simpld	$⊢ (φ \land ψ) \to D \in ⋃_{n \in ω} (A^{n})$
27		eliun	$⊢ D \in ⋃_{n \in ω} (A^{n}) \leftrightarrow \exists n \in ω D \in (A^{n})$
28	26 27	sylib	$⊢ (φ \land ψ) \to \exists n \in ω D \in (A^{n})$
29		elmapi	$⊢ D \in (A^{n}) \to D : n ⟶ A$
30	29	ad2antll	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to D : n ⟶ A$
31		ssiun2	$⊢ n \in ω \to x^{n} \subseteq ⋃_{n \in ω} (x^{n})$
32	31	ad2antrl	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to x^{n} \subseteq ⋃_{n \in ω} (x^{n})$
33	25	simprd	$⊢ (φ \land ψ) \to \neg D \in ⋃_{n \in ω} (x^{n})$
34	33	adantr	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to \neg D \in ⋃_{n \in ω} (x^{n})$
35	32 34	ssneldd	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to \neg D \in (x^{n})$
36		vex	$⊢ n \in V$
37	8 36	elmap	$⊢ D \in (x^{n}) \leftrightarrow D : n ⟶ x$
38		ffn	$⊢ D : n ⟶ A \to D Fn n$
39		ffnfv	$⊢ D : n ⟶ x \leftrightarrow (D Fn n \land \forall z \in n D (z) \in x)$
40	39	baib	$⊢ D Fn n \to (D : n ⟶ x \leftrightarrow \forall z \in n D (z) \in x)$
41	30 38 40	3syl	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to (D : n ⟶ x \leftrightarrow \forall z \in n D (z) \in x)$
42	37 41	syl5bb	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to (D \in (x^{n}) \leftrightarrow \forall z \in n D (z) \in x)$
43	35 42	mtbid	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to \neg \forall z \in n D (z) \in x$
44		nnon	$⊢ n \in ω \to n \in On$
45	44	ad2antrl	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to n \in On$
46		ssrab2	$⊢ \{z \in ω \| \neg D (z) \in x\} \subseteq ω$
47		omsson	$⊢ ω \subseteq On$
48	46 47	sstri	$⊢ \{z \in ω \| \neg D (z) \in x\} \subseteq On$
49		ordom	$⊢ Ord ω$
50		simprl	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to n \in ω$
51		ordelss	$⊢ (Ord ω \land n \in ω) \to n \subseteq ω$
52	49 50 51	sylancr	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to n \subseteq ω$
53		rexnal	$⊢ \exists z \in n \neg D (z) \in x \leftrightarrow \neg \forall z \in n D (z) \in x$
54	43 53	sylibr	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to \exists z \in n \neg D (z) \in x$
55		ssrexv	$⊢ n \subseteq ω \to (\exists z \in n \neg D (z) \in x \to \exists z \in ω \neg D (z) \in x)$
56	52 54 55	sylc	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to \exists z \in ω \neg D (z) \in x$
57		rabn0	$⊢ \{z \in ω \| \neg D (z) \in x\} \neq \emptyset \leftrightarrow \exists z \in ω \neg D (z) \in x$
58	56 57	sylibr	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to \{z \in ω \| \neg D (z) \in x\} \neq \emptyset$
59		onint	$⊢ (\{z \in ω \| \neg D (z) \in x\} \subseteq On \land \{z \in ω \| \neg D (z) \in x\} \neq \emptyset) \to ⋂ \{z \in ω \| \neg D (z) \in x\} \in \{z \in ω \| \neg D (z) \in x\}$
60	48 58 59	sylancr	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to ⋂ \{z \in ω \| \neg D (z) \in x\} \in \{z \in ω \| \neg D (z) \in x\}$
61	48 60	sselid	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to ⋂ \{z \in ω \| \neg D (z) \in x\} \in On$
62		ontri1	$⊢ (n \in On \land ⋂ \{z \in ω \| \neg D (z) \in x\} \in On) \to (n \subseteq ⋂ \{z \in ω \| \neg D (z) \in x\} \leftrightarrow \neg ⋂ \{z \in ω \| \neg D (z) \in x\} \in n)$
63	45 61 62	syl2anc	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to (n \subseteq ⋂ \{z \in ω \| \neg D (z) \in x\} \leftrightarrow \neg ⋂ \{z \in ω \| \neg D (z) \in x\} \in n)$
64		ssintrab	$⊢ n \subseteq ⋂ \{z \in ω \| \neg D (z) \in x\} \leftrightarrow \forall z \in ω (\neg D (z) \in x \to n \subseteq z)$
65		nnon	$⊢ z \in ω \to z \in On$
66		ontri1	$⊢ (n \in On \land z \in On) \to (n \subseteq z \leftrightarrow \neg z \in n)$
67	44 65 66	syl2an	$⊢ (n \in ω \land z \in ω) \to (n \subseteq z \leftrightarrow \neg z \in n)$
68	67	imbi2d	$⊢ (n \in ω \land z \in ω) \to ((\neg D (z) \in x \to n \subseteq z) \leftrightarrow (\neg D (z) \in x \to \neg z \in n))$
69		con34b	$⊢ (z \in n \to D (z) \in x) \leftrightarrow (\neg D (z) \in x \to \neg z \in n)$
70	68 69	bitr4di	$⊢ (n \in ω \land z \in ω) \to ((\neg D (z) \in x \to n \subseteq z) \leftrightarrow (z \in n \to D (z) \in x))$
71	70	pm5.74da	$⊢ n \in ω \to ((z \in ω \to (\neg D (z) \in x \to n \subseteq z)) \leftrightarrow (z \in ω \to (z \in n \to D (z) \in x)))$
72		bi2.04	$⊢ (z \in ω \to (z \in n \to D (z) \in x)) \leftrightarrow (z \in n \to (z \in ω \to D (z) \in x))$
73	71 72	bitrdi	$⊢ n \in ω \to ((z \in ω \to (\neg D (z) \in x \to n \subseteq z)) \leftrightarrow (z \in n \to (z \in ω \to D (z) \in x)))$
74		elnn	$⊢ (z \in n \land n \in ω) \to z \in ω$
75		pm2.27	$⊢ z \in ω \to ((z \in ω \to D (z) \in x) \to D (z) \in x)$
76	74 75	syl	$⊢ (z \in n \land n \in ω) \to ((z \in ω \to D (z) \in x) \to D (z) \in x)$
77	76	expcom	$⊢ n \in ω \to (z \in n \to ((z \in ω \to D (z) \in x) \to D (z) \in x))$
78	77	a2d	$⊢ n \in ω \to ((z \in n \to (z \in ω \to D (z) \in x)) \to (z \in n \to D (z) \in x))$
79	73 78	sylbid	$⊢ n \in ω \to ((z \in ω \to (\neg D (z) \in x \to n \subseteq z)) \to (z \in n \to D (z) \in x))$
80	79	ad2antrl	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to ((z \in ω \to (\neg D (z) \in x \to n \subseteq z)) \to (z \in n \to D (z) \in x))$
81	80	ralimdv2	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to (\forall z \in ω (\neg D (z) \in x \to n \subseteq z) \to \forall z \in n D (z) \in x)$
82	64 81	syl5bi	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to (n \subseteq ⋂ \{z \in ω \| \neg D (z) \in x\} \to \forall z \in n D (z) \in x)$
83	63 82	sylbird	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to (\neg ⋂ \{z \in ω \| \neg D (z) \in x\} \in n \to \forall z \in n D (z) \in x)$
84	43 83	mt3d	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to ⋂ \{z \in ω \| \neg D (z) \in x\} \in n$
85	30 84	ffvelrnd	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to D (⋂ \{z \in ω \| \neg D (z) \in x\}) \in A$
86		fveq2	$⊢ y = ⋂ \{z \in ω \| \neg D (z) \in x\} \to D (y) = D (⋂ \{z \in ω \| \neg D (z) \in x\})$
87	86	eleq1d	$⊢ y = ⋂ \{z \in ω \| \neg D (z) \in x\} \to (D (y) \in x \leftrightarrow D (⋂ \{z \in ω \| \neg D (z) \in x\}) \in x)$
88	87	notbid	$⊢ y = ⋂ \{z \in ω \| \neg D (z) \in x\} \to (\neg D (y) \in x \leftrightarrow \neg D (⋂ \{z \in ω \| \neg D (z) \in x\}) \in x)$
89		fveq2	$⊢ z = y \to D (z) = D (y)$
90	89	eleq1d	$⊢ z = y \to (D (z) \in x \leftrightarrow D (y) \in x)$
91	90	notbid	$⊢ z = y \to (\neg D (z) \in x \leftrightarrow \neg D (y) \in x)$
92	91	cbvrabv	$⊢ \{z \in ω \| \neg D (z) \in x\} = \{y \in ω \| \neg D (y) \in x\}$
93	88 92	elrab2	$⊢ ⋂ \{z \in ω \| \neg D (z) \in x\} \in \{z \in ω \| \neg D (z) \in x\} \leftrightarrow (⋂ \{z \in ω \| \neg D (z) \in x\} \in ω \land \neg D (⋂ \{z \in ω \| \neg D (z) \in x\}) \in x)$
94	93	simprbi	$⊢ ⋂ \{z \in ω \| \neg D (z) \in x\} \in \{z \in ω \| \neg D (z) \in x\} \to \neg D (⋂ \{z \in ω \| \neg D (z) \in x\}) \in x$
95	60 94	syl	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to \neg D (⋂ \{z \in ω \| \neg D (z) \in x\}) \in x$
96	85 95	eldifd	$⊢ ((φ \land ψ) \land (n \in ω \land D \in (A^{n}))) \to D (⋂ \{z \in ω \| \neg D (z) \in x\}) \in (A ∖ x)$
97	28 96	rexlimddv	$⊢ (φ \land ψ) \to D (⋂ \{z \in ω \| \neg D (z) \in x\}) \in (A ∖ x)$
98	22 97	eqeltrd	$⊢ (φ \land ψ) \to x F r \in (A ∖ x)$

Metamath Proof Explorer

Theorem pwfseqlem3

Proof