pwfseqlem1

Description: Lemma for pwfseq . Derive a contradiction by diagonalization. (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)))\})$
Assertion	pwfseqlem1	$⊢ (φ \land ψ) \to D \in (⋃_{n \in ω} (A^{n}) ∖ ⋃_{n \in ω} (x^{n}))$

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	1	adantr	$⊢ (φ \land ψ) \to G : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n})$
8		f1f	$⊢ G : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n}) \to G : 𝒫 A ⟶ ⋃_{n \in ω} (A^{n})$
9	7 8	syl	$⊢ (φ \land ψ) \to G : 𝒫 A ⟶ ⋃_{n \in ω} (A^{n})$
10		ssrab2	$⊢ \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\} \subseteq x$
11		simprl1	$⊢ (φ \land ((x \subseteq A \land r \subseteq x \times x \land r We x) \land ω ≼ x)) \to x \subseteq A$
12	4 11	sylan2b	$⊢ (φ \land ψ) \to x \subseteq A$
13	10 12	sstrid	$⊢ (φ \land ψ) \to \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\} \subseteq A$
14		vex	$⊢ x \in V$
15	14	rabex	$⊢ \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\} \in V$
16	15	elpw	$⊢ \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\} \in 𝒫 A \leftrightarrow \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\} \subseteq A$
17	13 16	sylibr	$⊢ (φ \land ψ) \to \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\} \in 𝒫 A$
18	9 17	ffvelrnd	$⊢ (φ \land ψ) \to G (\{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\}) \in ⋃_{n \in ω} (A^{n})$
19	6 18	eqeltrid	$⊢ (φ \land ψ) \to D \in ⋃_{n \in ω} (A^{n})$
20		pm5.19	$⊢ \neg (K (D) \in \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\} \leftrightarrow \neg K (D) \in \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\})$
21	5	adantr	$⊢ ((φ \land ψ) \land D \in ⋃_{n \in ω} (x^{n})) \to K : ⋃_{n \in ω} (x^{n}) \underset{1-1}{⟶} x$
22		f1f	$⊢ K : ⋃_{n \in ω} (x^{n}) \underset{1-1}{⟶} x \to K : ⋃_{n \in ω} (x^{n}) ⟶ x$
23	21 22	syl	$⊢ ((φ \land ψ) \land D \in ⋃_{n \in ω} (x^{n})) \to K : ⋃_{n \in ω} (x^{n}) ⟶ x$
24		ffvelrn	$⊢ (K : ⋃_{n \in ω} (x^{n}) ⟶ x \land D \in ⋃_{n \in ω} (x^{n})) \to K (D) \in x$
25	23 24	sylancom	$⊢ ((φ \land ψ) \land D \in ⋃_{n \in ω} (x^{n})) \to K (D) \in x$
26		f1f1orn	$⊢ K : ⋃_{n \in ω} (x^{n}) \underset{1-1}{⟶} x \to K : ⋃_{n \in ω} (x^{n}) \underset{1-1 onto}{⟶} ran K$
27	21 26	syl	$⊢ ((φ \land ψ) \land D \in ⋃_{n \in ω} (x^{n})) \to K : ⋃_{n \in ω} (x^{n}) \underset{1-1 onto}{⟶} ran K$
28		f1ocnvfv1	$⊢ (K : ⋃_{n \in ω} (x^{n}) \underset{1-1 onto}{⟶} ran K \land D \in ⋃_{n \in ω} (x^{n})) \to K^{-1} (K (D)) = D$
29	27 28	sylancom	$⊢ ((φ \land ψ) \land D \in ⋃_{n \in ω} (x^{n})) \to K^{-1} (K (D)) = D$
30		f1fn	$⊢ G : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n}) \to G Fn 𝒫 A$
31	7 30	syl	$⊢ (φ \land ψ) \to G Fn 𝒫 A$
32		fnfvelrn	$⊢ (G Fn 𝒫 A \land \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\} \in 𝒫 A) \to G (\{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\}) \in ran G$
33	31 17 32	syl2anc	$⊢ (φ \land ψ) \to G (\{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\}) \in ran G$
34	6 33	eqeltrid	$⊢ (φ \land ψ) \to D \in ran G$
35	34	adantr	$⊢ ((φ \land ψ) \land D \in ⋃_{n \in ω} (x^{n})) \to D \in ran G$
36	29 35	eqeltrd	$⊢ ((φ \land ψ) \land D \in ⋃_{n \in ω} (x^{n})) \to K^{-1} (K (D)) \in ran G$
37		fveq2	$⊢ y = K (D) \to K^{-1} (y) = K^{-1} (K (D))$
38	37	eleq1d	$⊢ y = K (D) \to (K^{-1} (y) \in ran G \leftrightarrow K^{-1} (K (D)) \in ran G)$
39		id	$⊢ y = K (D) \to y = K (D)$
40		2fveq3	$⊢ y = K (D) \to G^{-1} (K^{-1} (y)) = G^{-1} (K^{-1} (K (D)))$
41	39 40	eleq12d	$⊢ y = K (D) \to (y \in G^{-1} (K^{-1} (y)) \leftrightarrow K (D) \in G^{-1} (K^{-1} (K (D))))$
42	41	notbid	$⊢ y = K (D) \to (\neg y \in G^{-1} (K^{-1} (y)) \leftrightarrow \neg K (D) \in G^{-1} (K^{-1} (K (D))))$
43	38 42	anbi12d	$⊢ y = K (D) \to ((K^{-1} (y) \in ran G \land \neg y \in G^{-1} (K^{-1} (y))) \leftrightarrow (K^{-1} (K (D)) \in ran G \land \neg K (D) \in G^{-1} (K^{-1} (K (D)))))$
44		fveq2	$⊢ w = y \to K^{-1} (w) = K^{-1} (y)$
45	44	eleq1d	$⊢ w = y \to (K^{-1} (w) \in ran G \leftrightarrow K^{-1} (y) \in ran G)$
46		id	$⊢ w = y \to w = y$
47		2fveq3	$⊢ w = y \to G^{-1} (K^{-1} (w)) = G^{-1} (K^{-1} (y))$
48	46 47	eleq12d	$⊢ w = y \to (w \in G^{-1} (K^{-1} (w)) \leftrightarrow y \in G^{-1} (K^{-1} (y)))$
49	48	notbid	$⊢ w = y \to (\neg w \in G^{-1} (K^{-1} (w)) \leftrightarrow \neg y \in G^{-1} (K^{-1} (y)))$
50	45 49	anbi12d	$⊢ w = y \to ((K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w))) \leftrightarrow (K^{-1} (y) \in ran G \land \neg y \in G^{-1} (K^{-1} (y))))$
51	50	cbvrabv	$⊢ \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\} = \{y \in x \| (K^{-1} (y) \in ran G \land \neg y \in G^{-1} (K^{-1} (y)))\}$
52	43 51	elrab2	$⊢ K (D) \in \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\} \leftrightarrow (K (D) \in x \land (K^{-1} (K (D)) \in ran G \land \neg K (D) \in G^{-1} (K^{-1} (K (D)))))$
53		anass	$⊢ ((K (D) \in x \land K^{-1} (K (D)) \in ran G) \land \neg K (D) \in G^{-1} (K^{-1} (K (D)))) \leftrightarrow (K (D) \in x \land (K^{-1} (K (D)) \in ran G \land \neg K (D) \in G^{-1} (K^{-1} (K (D)))))$
54	52 53	bitr4i	$⊢ K (D) \in \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\} \leftrightarrow ((K (D) \in x \land K^{-1} (K (D)) \in ran G) \land \neg K (D) \in G^{-1} (K^{-1} (K (D))))$
55	54	baib	$⊢ (K (D) \in x \land K^{-1} (K (D)) \in ran G) \to (K (D) \in \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\} \leftrightarrow \neg K (D) \in G^{-1} (K^{-1} (K (D))))$
56	25 36 55	syl2anc	$⊢ ((φ \land ψ) \land D \in ⋃_{n \in ω} (x^{n})) \to (K (D) \in \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\} \leftrightarrow \neg K (D) \in G^{-1} (K^{-1} (K (D))))$
57	29 6	eqtrdi	$⊢ ((φ \land ψ) \land D \in ⋃_{n \in ω} (x^{n})) \to K^{-1} (K (D)) = G (\{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\})$
58	57	fveq2d	$⊢ ((φ \land ψ) \land D \in ⋃_{n \in ω} (x^{n})) \to G^{-1} (K^{-1} (K (D))) = G^{-1} (G (\{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\}))$
59		f1f1orn	$⊢ G : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n}) \to G : 𝒫 A \underset{1-1 onto}{⟶} ran G$
60	7 59	syl	$⊢ (φ \land ψ) \to G : 𝒫 A \underset{1-1 onto}{⟶} ran G$
61		f1ocnvfv1	$⊢ (G : 𝒫 A \underset{1-1 onto}{⟶} ran G \land \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\} \in 𝒫 A) \to G^{-1} (G (\{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\})) = \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\}$
62	60 17 61	syl2anc	$⊢ (φ \land ψ) \to G^{-1} (G (\{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\})) = \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\}$
63	62	adantr	$⊢ ((φ \land ψ) \land D \in ⋃_{n \in ω} (x^{n})) \to G^{-1} (G (\{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\})) = \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\}$
64	58 63	eqtrd	$⊢ ((φ \land ψ) \land D \in ⋃_{n \in ω} (x^{n})) \to G^{-1} (K^{-1} (K (D))) = \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\}$
65	64	eleq2d	$⊢ ((φ \land ψ) \land D \in ⋃_{n \in ω} (x^{n})) \to (K (D) \in G^{-1} (K^{-1} (K (D))) \leftrightarrow K (D) \in \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\})$
66	65	notbid	$⊢ ((φ \land ψ) \land D \in ⋃_{n \in ω} (x^{n})) \to (\neg K (D) \in G^{-1} (K^{-1} (K (D))) \leftrightarrow \neg K (D) \in \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\})$
67	56 66	bitrd	$⊢ ((φ \land ψ) \land D \in ⋃_{n \in ω} (x^{n})) \to (K (D) \in \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\} \leftrightarrow \neg K (D) \in \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\})$
68	67	ex	$⊢ (φ \land ψ) \to (D \in ⋃_{n \in ω} (x^{n}) \to (K (D) \in \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\} \leftrightarrow \neg K (D) \in \{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\}))$
69	20 68	mtoi	$⊢ (φ \land ψ) \to \neg D \in ⋃_{n \in ω} (x^{n})$
70	19 69	eldifd	$⊢ (φ \land ψ) \to D \in (⋃_{n \in ω} (A^{n}) ∖ ⋃_{n \in ω} (x^{n}))$

Metamath Proof Explorer

Theorem pwfseqlem1

Proof