MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  knatar Structured version   Visualization version   GIF version

Theorem knatar 7166
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 𝒫 𝐴. (Contributed by Mario Carneiro, 11-Jun-2015.)
Hypothesis
Ref Expression
knatar.1 𝑋 = {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧}
Assertion
Ref Expression
knatar ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝑋𝐴 ∧ (𝐹𝑋) = 𝑋))
Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐹,𝑦,𝑧   𝑥,𝑋,𝑦
Allowed substitution hints:   𝑉(𝑥,𝑦,𝑧)   𝑋(𝑧)

Proof of Theorem knatar
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 knatar.1 . . 3 𝑋 = {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧}
2 pwidg 4535 . . . . 5 (𝐴𝑉𝐴 ∈ 𝒫 𝐴)
323ad2ant1 1135 . . . 4 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → 𝐴 ∈ 𝒫 𝐴)
4 simp2 1139 . . . 4 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝐴) ⊆ 𝐴)
5 fveq2 6717 . . . . . 6 (𝑧 = 𝐴 → (𝐹𝑧) = (𝐹𝐴))
6 id 22 . . . . . 6 (𝑧 = 𝐴𝑧 = 𝐴)
75, 6sseq12d 3934 . . . . 5 (𝑧 = 𝐴 → ((𝐹𝑧) ⊆ 𝑧 ↔ (𝐹𝐴) ⊆ 𝐴))
87intminss 4885 . . . 4 ((𝐴 ∈ 𝒫 𝐴 ∧ (𝐹𝐴) ⊆ 𝐴) → {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} ⊆ 𝐴)
93, 4, 8syl2anc 587 . . 3 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} ⊆ 𝐴)
101, 9eqsstrid 3949 . 2 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → 𝑋𝐴)
11 fveq2 6717 . . . . . . . . . 10 (𝑦 = 𝑋 → (𝐹𝑦) = (𝐹𝑋))
1211sseq1d 3932 . . . . . . . . 9 (𝑦 = 𝑋 → ((𝐹𝑦) ⊆ (𝐹𝑤) ↔ (𝐹𝑋) ⊆ (𝐹𝑤)))
13 pweq 4529 . . . . . . . . . . 11 (𝑥 = 𝑤 → 𝒫 𝑥 = 𝒫 𝑤)
14 fveq2 6717 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝐹𝑥) = (𝐹𝑤))
1514sseq2d 3933 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((𝐹𝑦) ⊆ (𝐹𝑥) ↔ (𝐹𝑦) ⊆ (𝐹𝑤)))
1613, 15raleqbidv 3313 . . . . . . . . . 10 (𝑥 = 𝑤 → (∀𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥) ↔ ∀𝑦 ∈ 𝒫 𝑤(𝐹𝑦) ⊆ (𝐹𝑤)))
17 simpl3 1195 . . . . . . . . . 10 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥))
18 simprl 771 . . . . . . . . . 10 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → 𝑤 ∈ 𝒫 𝐴)
1916, 17, 18rspcdva 3539 . . . . . . . . 9 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → ∀𝑦 ∈ 𝒫 𝑤(𝐹𝑦) ⊆ (𝐹𝑤))
20 fveq2 6717 . . . . . . . . . . . . . 14 (𝑧 = 𝑤 → (𝐹𝑧) = (𝐹𝑤))
21 id 22 . . . . . . . . . . . . . 14 (𝑧 = 𝑤𝑧 = 𝑤)
2220, 21sseq12d 3934 . . . . . . . . . . . . 13 (𝑧 = 𝑤 → ((𝐹𝑧) ⊆ 𝑧 ↔ (𝐹𝑤) ⊆ 𝑤))
2322intminss 4885 . . . . . . . . . . . 12 ((𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤) → {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} ⊆ 𝑤)
2423adantl 485 . . . . . . . . . . 11 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} ⊆ 𝑤)
251, 24eqsstrid 3949 . . . . . . . . . 10 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → 𝑋𝑤)
26 vex 3412 . . . . . . . . . . 11 𝑤 ∈ V
2726elpw2 5238 . . . . . . . . . 10 (𝑋 ∈ 𝒫 𝑤𝑋𝑤)
2825, 27sylibr 237 . . . . . . . . 9 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → 𝑋 ∈ 𝒫 𝑤)
2912, 19, 28rspcdva 3539 . . . . . . . 8 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → (𝐹𝑋) ⊆ (𝐹𝑤))
30 simprr 773 . . . . . . . 8 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → (𝐹𝑤) ⊆ 𝑤)
3129, 30sstrd 3911 . . . . . . 7 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → (𝐹𝑋) ⊆ 𝑤)
3231expr 460 . . . . . 6 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ 𝑤 ∈ 𝒫 𝐴) → ((𝐹𝑤) ⊆ 𝑤 → (𝐹𝑋) ⊆ 𝑤))
3332ralrimiva 3105 . . . . 5 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → ∀𝑤 ∈ 𝒫 𝐴((𝐹𝑤) ⊆ 𝑤 → (𝐹𝑋) ⊆ 𝑤))
34 ssintrab 4882 . . . . 5 ((𝐹𝑋) ⊆ {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤} ↔ ∀𝑤 ∈ 𝒫 𝐴((𝐹𝑤) ⊆ 𝑤 → (𝐹𝑋) ⊆ 𝑤))
3533, 34sylibr 237 . . . 4 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ⊆ {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤})
3622cbvrabv 3402 . . . . . 6 {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} = {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤}
3736inteqi 4863 . . . . 5 {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} = {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤}
381, 37eqtri 2765 . . . 4 𝑋 = {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤}
3935, 38sseqtrrdi 3952 . . 3 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ⊆ 𝑋)
4011sseq1d 3932 . . . . . . . 8 (𝑦 = 𝑋 → ((𝐹𝑦) ⊆ (𝐹𝐴) ↔ (𝐹𝑋) ⊆ (𝐹𝐴)))
41 pweq 4529 . . . . . . . . . 10 (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
42 fveq2 6717 . . . . . . . . . . 11 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
4342sseq2d 3933 . . . . . . . . . 10 (𝑥 = 𝐴 → ((𝐹𝑦) ⊆ (𝐹𝑥) ↔ (𝐹𝑦) ⊆ (𝐹𝐴)))
4441, 43raleqbidv 3313 . . . . . . . . 9 (𝑥 = 𝐴 → (∀𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥) ↔ ∀𝑦 ∈ 𝒫 𝐴(𝐹𝑦) ⊆ (𝐹𝐴)))
45 simp3 1140 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥))
4644, 45, 3rspcdva 3539 . . . . . . . 8 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → ∀𝑦 ∈ 𝒫 𝐴(𝐹𝑦) ⊆ (𝐹𝐴))
473, 10sselpwd 5219 . . . . . . . 8 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → 𝑋 ∈ 𝒫 𝐴)
4840, 46, 47rspcdva 3539 . . . . . . 7 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ⊆ (𝐹𝐴))
4948, 4sstrd 3911 . . . . . 6 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ⊆ 𝐴)
50 fvex 6730 . . . . . . 7 (𝐹𝑋) ∈ V
5150elpw 4517 . . . . . 6 ((𝐹𝑋) ∈ 𝒫 𝐴 ↔ (𝐹𝑋) ⊆ 𝐴)
5249, 51sylibr 237 . . . . 5 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ∈ 𝒫 𝐴)
53 fveq2 6717 . . . . . . 7 (𝑦 = (𝐹𝑋) → (𝐹𝑦) = (𝐹‘(𝐹𝑋)))
5453sseq1d 3932 . . . . . 6 (𝑦 = (𝐹𝑋) → ((𝐹𝑦) ⊆ (𝐹𝑋) ↔ (𝐹‘(𝐹𝑋)) ⊆ (𝐹𝑋)))
55 pweq 4529 . . . . . . . 8 (𝑥 = 𝑋 → 𝒫 𝑥 = 𝒫 𝑋)
56 fveq2 6717 . . . . . . . . 9 (𝑥 = 𝑋 → (𝐹𝑥) = (𝐹𝑋))
5756sseq2d 3933 . . . . . . . 8 (𝑥 = 𝑋 → ((𝐹𝑦) ⊆ (𝐹𝑥) ↔ (𝐹𝑦) ⊆ (𝐹𝑋)))
5855, 57raleqbidv 3313 . . . . . . 7 (𝑥 = 𝑋 → (∀𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥) ↔ ∀𝑦 ∈ 𝒫 𝑋(𝐹𝑦) ⊆ (𝐹𝑋)))
5958, 45, 47rspcdva 3539 . . . . . 6 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → ∀𝑦 ∈ 𝒫 𝑋(𝐹𝑦) ⊆ (𝐹𝑋))
6050elpw 4517 . . . . . . 7 ((𝐹𝑋) ∈ 𝒫 𝑋 ↔ (𝐹𝑋) ⊆ 𝑋)
6139, 60sylibr 237 . . . . . 6 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ∈ 𝒫 𝑋)
6254, 59, 61rspcdva 3539 . . . . 5 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹‘(𝐹𝑋)) ⊆ (𝐹𝑋))
63 fveq2 6717 . . . . . . 7 (𝑤 = (𝐹𝑋) → (𝐹𝑤) = (𝐹‘(𝐹𝑋)))
64 id 22 . . . . . . 7 (𝑤 = (𝐹𝑋) → 𝑤 = (𝐹𝑋))
6563, 64sseq12d 3934 . . . . . 6 (𝑤 = (𝐹𝑋) → ((𝐹𝑤) ⊆ 𝑤 ↔ (𝐹‘(𝐹𝑋)) ⊆ (𝐹𝑋)))
6665intminss 4885 . . . . 5 (((𝐹𝑋) ∈ 𝒫 𝐴 ∧ (𝐹‘(𝐹𝑋)) ⊆ (𝐹𝑋)) → {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤} ⊆ (𝐹𝑋))
6752, 62, 66syl2anc 587 . . . 4 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤} ⊆ (𝐹𝑋))
6838, 67eqsstrid 3949 . . 3 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → 𝑋 ⊆ (𝐹𝑋))
6939, 68eqssd 3918 . 2 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) = 𝑋)
7010, 69jca 515 1 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝑋𝐴 ∧ (𝐹𝑋) = 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1089   = wceq 1543  wcel 2110  wral 3061  {crab 3065  wss 3866  𝒫 cpw 4513   cint 4859  cfv 6380
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-int 4860  df-br 5054  df-iota 6338  df-fv 6388
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator