Metamath Proof Explorer

Theorem 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 e. ~P A | ( F ` z ) C_ z }
Assertion knatar 
|- ( ( A e. V /\ ( F ` A ) C_ A /\ A. x e. ~P A A. y e. ~P x ( F ` y ) C_ ( F ` x ) ) -> ( X C_ A /\ ( F ` X ) = X ) )

Proof

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