knatar

Description: The Knaster-Tarski theorem says that every monotone function over a complete lattice has a (least) fixpoint. Here we specialize this theorem to the case when the lattice is the powerset lattice ~P A . (Contributed by Mario Carneiro, 11-Jun-2015)

		Ref	Expression
	Hypothesis	knatar.1	$⊢ X = ⋂ \{z \in 𝒫 A \| F (z) \subseteq z\}$
	Assertion	knatar	$⊢ (A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \to (X \subseteq A \land F (X) = X)$

Proof

Step	Hyp	Ref	Expression
1		knatar.1	$⊢ X = ⋂ \{z \in 𝒫 A \| F (z) \subseteq z\}$
2		pwidg	$⊢ A \in V \to A \in 𝒫 A$
3	2	3ad2ant1	$⊢ (A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \to A \in 𝒫 A$
4		simp2	$⊢ (A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \to F (A) \subseteq A$
5		fveq2	$⊢ z = A \to F (z) = F (A)$
6		id	$⊢ z = A \to z = A$
7	5 6	sseq12d	$⊢ z = A \to (F (z) \subseteq z \leftrightarrow F (A) \subseteq A)$
8	7	intminss	$⊢ (A \in 𝒫 A \land F (A) \subseteq A) \to ⋂ \{z \in 𝒫 A \| F (z) \subseteq z\} \subseteq A$
9	3 4 8	syl2anc	$⊢ (A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \to ⋂ \{z \in 𝒫 A \| F (z) \subseteq z\} \subseteq A$
10	1 9	eqsstrid	$⊢ (A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \to X \subseteq A$
11		fveq2	$⊢ y = X \to F (y) = F (X)$
12	11	sseq1d	$⊢ y = X \to (F (y) \subseteq F (w) \leftrightarrow F (X) \subseteq F (w))$
13		pweq	$⊢ x = w \to 𝒫 x = 𝒫 w$
14		fveq2	$⊢ x = w \to F (x) = F (w)$
15	14	sseq2d	$⊢ x = w \to (F (y) \subseteq F (x) \leftrightarrow F (y) \subseteq F (w))$
16	13 15	raleqbidv	$⊢ x = w \to (\forall y \in 𝒫 x F (y) \subseteq F (x) \leftrightarrow \forall y \in 𝒫 w F (y) \subseteq F (w))$
17		simpl3	$⊢ ((A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \land (w \in 𝒫 A \land F (w) \subseteq w)) \to \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)$
18		simprl	$⊢ ((A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \land (w \in 𝒫 A \land F (w) \subseteq w)) \to w \in 𝒫 A$
19	16 17 18	rspcdva	$⊢ ((A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \land (w \in 𝒫 A \land F (w) \subseteq w)) \to \forall y \in 𝒫 w F (y) \subseteq F (w)$
20		fveq2	$⊢ z = w \to F (z) = F (w)$
21		id	$⊢ z = w \to z = w$
22	20 21	sseq12d	$⊢ z = w \to (F (z) \subseteq z \leftrightarrow F (w) \subseteq w)$
23	22	intminss	$⊢ (w \in 𝒫 A \land F (w) \subseteq w) \to ⋂ \{z \in 𝒫 A \| F (z) \subseteq z\} \subseteq w$
24	23	adantl	$⊢ ((A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \land (w \in 𝒫 A \land F (w) \subseteq w)) \to ⋂ \{z \in 𝒫 A \| F (z) \subseteq z\} \subseteq w$
25	1 24	eqsstrid	$⊢ ((A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \land (w \in 𝒫 A \land F (w) \subseteq w)) \to X \subseteq w$
26		vex	$⊢ w \in V$
27	26	elpw2	$⊢ X \in 𝒫 w \leftrightarrow X \subseteq w$
28	25 27	sylibr	$⊢ ((A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \land (w \in 𝒫 A \land F (w) \subseteq w)) \to X \in 𝒫 w$
29	12 19 28	rspcdva	$⊢ ((A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \land (w \in 𝒫 A \land F (w) \subseteq w)) \to F (X) \subseteq F (w)$
30		simprr	$⊢ ((A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \land (w \in 𝒫 A \land F (w) \subseteq w)) \to F (w) \subseteq w$
31	29 30	sstrd	$⊢ ((A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \land (w \in 𝒫 A \land F (w) \subseteq w)) \to F (X) \subseteq w$
32	31	expr	$⊢ ((A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \land w \in 𝒫 A) \to (F (w) \subseteq w \to F (X) \subseteq w)$
33	32	ralrimiva	$⊢ (A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \to \forall w \in 𝒫 A (F (w) \subseteq w \to F (X) \subseteq w)$
34		ssintrab	$⊢ F (X) \subseteq ⋂ \{w \in 𝒫 A \| F (w) \subseteq w\} \leftrightarrow \forall w \in 𝒫 A (F (w) \subseteq w \to F (X) \subseteq w)$
35	33 34	sylibr	$⊢ (A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \to F (X) \subseteq ⋂ \{w \in 𝒫 A \| F (w) \subseteq w\}$
36	22	cbvrabv	$⊢ \{z \in 𝒫 A \| F (z) \subseteq z\} = \{w \in 𝒫 A \| F (w) \subseteq w\}$
37	36	inteqi	$⊢ ⋂ \{z \in 𝒫 A \| F (z) \subseteq z\} = ⋂ \{w \in 𝒫 A \| F (w) \subseteq w\}$
38	1 37	eqtri	$⊢ X = ⋂ \{w \in 𝒫 A \| F (w) \subseteq w\}$
39	35 38	sseqtrrdi	$⊢ (A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \to F (X) \subseteq X$
40	11	sseq1d	$⊢ y = X \to (F (y) \subseteq F (A) \leftrightarrow F (X) \subseteq F (A))$
41		pweq	$⊢ x = A \to 𝒫 x = 𝒫 A$
42		fveq2	$⊢ x = A \to F (x) = F (A)$
43	42	sseq2d	$⊢ x = A \to (F (y) \subseteq F (x) \leftrightarrow F (y) \subseteq F (A))$
44	41 43	raleqbidv	$⊢ x = A \to (\forall y \in 𝒫 x F (y) \subseteq F (x) \leftrightarrow \forall y \in 𝒫 A F (y) \subseteq F (A))$
45		simp3	$⊢ (A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \to \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)$
46	44 45 3	rspcdva	$⊢ (A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \to \forall y \in 𝒫 A F (y) \subseteq F (A)$
47	3 10	sselpwd	$⊢ (A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \to X \in 𝒫 A$
48	40 46 47	rspcdva	$⊢ (A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \to F (X) \subseteq F (A)$
49	48 4	sstrd	$⊢ (A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \to F (X) \subseteq A$
50		fvex	$⊢ F (X) \in V$
51	50	elpw	$⊢ F (X) \in 𝒫 A \leftrightarrow F (X) \subseteq A$
52	49 51	sylibr	$⊢ (A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \to F (X) \in 𝒫 A$
53		fveq2	$⊢ y = F (X) \to F (y) = F (F (X))$
54	53	sseq1d	$⊢ y = F (X) \to (F (y) \subseteq F (X) \leftrightarrow F (F (X)) \subseteq F (X))$
55		pweq	$⊢ x = X \to 𝒫 x = 𝒫 X$
56		fveq2	$⊢ x = X \to F (x) = F (X)$
57	56	sseq2d	$⊢ x = X \to (F (y) \subseteq F (x) \leftrightarrow F (y) \subseteq F (X))$
58	55 57	raleqbidv	$⊢ x = X \to (\forall y \in 𝒫 x F (y) \subseteq F (x) \leftrightarrow \forall y \in 𝒫 X F (y) \subseteq F (X))$
59	58 45 47	rspcdva	$⊢ (A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \to \forall y \in 𝒫 X F (y) \subseteq F (X)$
60	50	elpw	$⊢ F (X) \in 𝒫 X \leftrightarrow F (X) \subseteq X$
61	39 60	sylibr	$⊢ (A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \to F (X) \in 𝒫 X$
62	54 59 61	rspcdva	$⊢ (A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \to F (F (X)) \subseteq F (X)$
63		fveq2	$⊢ w = F (X) \to F (w) = F (F (X))$
64		id	$⊢ w = F (X) \to w = F (X)$
65	63 64	sseq12d	$⊢ w = F (X) \to (F (w) \subseteq w \leftrightarrow F (F (X)) \subseteq F (X))$
66	65	intminss	$⊢ (F (X) \in 𝒫 A \land F (F (X)) \subseteq F (X)) \to ⋂ \{w \in 𝒫 A \| F (w) \subseteq w\} \subseteq F (X)$
67	52 62 66	syl2anc	$⊢ (A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \to ⋂ \{w \in 𝒫 A \| F (w) \subseteq w\} \subseteq F (X)$
68	38 67	eqsstrid	$⊢ (A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \to X \subseteq F (X)$
69	39 68	eqssd	$⊢ (A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \to F (X) = X$
70	10 69	jca	$⊢ (A \in V \land F (A) \subseteq A \land \forall x \in 𝒫 A \forall y \in 𝒫 x F (y) \subseteq F (x)) \to (X \subseteq A \land F (X) = X)$

Metamath Proof Explorer

Theorem knatar

Proof