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

Theorem knatar 7354
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 4623 . . . . 5 (𝐴𝑉𝐴 ∈ 𝒫 𝐴)
323ad2ant1 1134 . . . 4 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → 𝐴 ∈ 𝒫 𝐴)
4 simp2 1138 . . . 4 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝐴) ⊆ 𝐴)
5 fveq2 6892 . . . . . 6 (𝑧 = 𝐴 → (𝐹𝑧) = (𝐹𝐴))
6 id 22 . . . . . 6 (𝑧 = 𝐴𝑧 = 𝐴)
75, 6sseq12d 4016 . . . . 5 (𝑧 = 𝐴 → ((𝐹𝑧) ⊆ 𝑧 ↔ (𝐹𝐴) ⊆ 𝐴))
87intminss 4979 . . . 4 ((𝐴 ∈ 𝒫 𝐴 ∧ (𝐹𝐴) ⊆ 𝐴) → {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} ⊆ 𝐴)
93, 4, 8syl2anc 585 . . 3 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} ⊆ 𝐴)
101, 9eqsstrid 4031 . 2 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → 𝑋𝐴)
11 fveq2 6892 . . . . . . . . . 10 (𝑦 = 𝑋 → (𝐹𝑦) = (𝐹𝑋))
1211sseq1d 4014 . . . . . . . . 9 (𝑦 = 𝑋 → ((𝐹𝑦) ⊆ (𝐹𝑤) ↔ (𝐹𝑋) ⊆ (𝐹𝑤)))
13 pweq 4617 . . . . . . . . . . 11 (𝑥 = 𝑤 → 𝒫 𝑥 = 𝒫 𝑤)
14 fveq2 6892 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝐹𝑥) = (𝐹𝑤))
1514sseq2d 4015 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((𝐹𝑦) ⊆ (𝐹𝑥) ↔ (𝐹𝑦) ⊆ (𝐹𝑤)))
1613, 15raleqbidv 3343 . . . . . . . . . 10 (𝑥 = 𝑤 → (∀𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥) ↔ ∀𝑦 ∈ 𝒫 𝑤(𝐹𝑦) ⊆ (𝐹𝑤)))
17 simpl3 1194 . . . . . . . . . 10 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥))
18 simprl 770 . . . . . . . . . 10 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → 𝑤 ∈ 𝒫 𝐴)
1916, 17, 18rspcdva 3614 . . . . . . . . 9 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → ∀𝑦 ∈ 𝒫 𝑤(𝐹𝑦) ⊆ (𝐹𝑤))
20 fveq2 6892 . . . . . . . . . . . . . 14 (𝑧 = 𝑤 → (𝐹𝑧) = (𝐹𝑤))
21 id 22 . . . . . . . . . . . . . 14 (𝑧 = 𝑤𝑧 = 𝑤)
2220, 21sseq12d 4016 . . . . . . . . . . . . 13 (𝑧 = 𝑤 → ((𝐹𝑧) ⊆ 𝑧 ↔ (𝐹𝑤) ⊆ 𝑤))
2322intminss 4979 . . . . . . . . . . . 12 ((𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤) → {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} ⊆ 𝑤)
2423adantl 483 . . . . . . . . . . 11 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} ⊆ 𝑤)
251, 24eqsstrid 4031 . . . . . . . . . 10 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → 𝑋𝑤)
26 vex 3479 . . . . . . . . . . 11 𝑤 ∈ V
2726elpw2 5346 . . . . . . . . . 10 (𝑋 ∈ 𝒫 𝑤𝑋𝑤)
2825, 27sylibr 233 . . . . . . . . 9 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → 𝑋 ∈ 𝒫 𝑤)
2912, 19, 28rspcdva 3614 . . . . . . . 8 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → (𝐹𝑋) ⊆ (𝐹𝑤))
30 simprr 772 . . . . . . . 8 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → (𝐹𝑤) ⊆ 𝑤)
3129, 30sstrd 3993 . . . . . . 7 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → (𝐹𝑋) ⊆ 𝑤)
3231expr 458 . . . . . 6 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ 𝑤 ∈ 𝒫 𝐴) → ((𝐹𝑤) ⊆ 𝑤 → (𝐹𝑋) ⊆ 𝑤))
3332ralrimiva 3147 . . . . 5 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → ∀𝑤 ∈ 𝒫 𝐴((𝐹𝑤) ⊆ 𝑤 → (𝐹𝑋) ⊆ 𝑤))
34 ssintrab 4976 . . . . 5 ((𝐹𝑋) ⊆ {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤} ↔ ∀𝑤 ∈ 𝒫 𝐴((𝐹𝑤) ⊆ 𝑤 → (𝐹𝑋) ⊆ 𝑤))
3533, 34sylibr 233 . . . 4 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ⊆ {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤})
3622cbvrabv 3443 . . . . . 6 {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} = {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤}
3736inteqi 4955 . . . . 5 {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} = {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤}
381, 37eqtri 2761 . . . 4 𝑋 = {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤}
3935, 38sseqtrrdi 4034 . . 3 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ⊆ 𝑋)
4011sseq1d 4014 . . . . . . . 8 (𝑦 = 𝑋 → ((𝐹𝑦) ⊆ (𝐹𝐴) ↔ (𝐹𝑋) ⊆ (𝐹𝐴)))
41 pweq 4617 . . . . . . . . . 10 (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
42 fveq2 6892 . . . . . . . . . . 11 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
4342sseq2d 4015 . . . . . . . . . 10 (𝑥 = 𝐴 → ((𝐹𝑦) ⊆ (𝐹𝑥) ↔ (𝐹𝑦) ⊆ (𝐹𝐴)))
4441, 43raleqbidv 3343 . . . . . . . . 9 (𝑥 = 𝐴 → (∀𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥) ↔ ∀𝑦 ∈ 𝒫 𝐴(𝐹𝑦) ⊆ (𝐹𝐴)))
45 simp3 1139 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥))
4644, 45, 3rspcdva 3614 . . . . . . . 8 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → ∀𝑦 ∈ 𝒫 𝐴(𝐹𝑦) ⊆ (𝐹𝐴))
473, 10sselpwd 5327 . . . . . . . 8 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → 𝑋 ∈ 𝒫 𝐴)
4840, 46, 47rspcdva 3614 . . . . . . 7 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ⊆ (𝐹𝐴))
4948, 4sstrd 3993 . . . . . 6 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ⊆ 𝐴)
50 fvex 6905 . . . . . . 7 (𝐹𝑋) ∈ V
5150elpw 4607 . . . . . 6 ((𝐹𝑋) ∈ 𝒫 𝐴 ↔ (𝐹𝑋) ⊆ 𝐴)
5249, 51sylibr 233 . . . . 5 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ∈ 𝒫 𝐴)
53 fveq2 6892 . . . . . . 7 (𝑦 = (𝐹𝑋) → (𝐹𝑦) = (𝐹‘(𝐹𝑋)))
5453sseq1d 4014 . . . . . 6 (𝑦 = (𝐹𝑋) → ((𝐹𝑦) ⊆ (𝐹𝑋) ↔ (𝐹‘(𝐹𝑋)) ⊆ (𝐹𝑋)))
55 pweq 4617 . . . . . . . 8 (𝑥 = 𝑋 → 𝒫 𝑥 = 𝒫 𝑋)
56 fveq2 6892 . . . . . . . . 9 (𝑥 = 𝑋 → (𝐹𝑥) = (𝐹𝑋))
5756sseq2d 4015 . . . . . . . 8 (𝑥 = 𝑋 → ((𝐹𝑦) ⊆ (𝐹𝑥) ↔ (𝐹𝑦) ⊆ (𝐹𝑋)))
5855, 57raleqbidv 3343 . . . . . . 7 (𝑥 = 𝑋 → (∀𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥) ↔ ∀𝑦 ∈ 𝒫 𝑋(𝐹𝑦) ⊆ (𝐹𝑋)))
5958, 45, 47rspcdva 3614 . . . . . 6 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → ∀𝑦 ∈ 𝒫 𝑋(𝐹𝑦) ⊆ (𝐹𝑋))
6050elpw 4607 . . . . . . 7 ((𝐹𝑋) ∈ 𝒫 𝑋 ↔ (𝐹𝑋) ⊆ 𝑋)
6139, 60sylibr 233 . . . . . 6 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ∈ 𝒫 𝑋)
6254, 59, 61rspcdva 3614 . . . . 5 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹‘(𝐹𝑋)) ⊆ (𝐹𝑋))
63 fveq2 6892 . . . . . . 7 (𝑤 = (𝐹𝑋) → (𝐹𝑤) = (𝐹‘(𝐹𝑋)))
64 id 22 . . . . . . 7 (𝑤 = (𝐹𝑋) → 𝑤 = (𝐹𝑋))
6563, 64sseq12d 4016 . . . . . 6 (𝑤 = (𝐹𝑋) → ((𝐹𝑤) ⊆ 𝑤 ↔ (𝐹‘(𝐹𝑋)) ⊆ (𝐹𝑋)))
6665intminss 4979 . . . . 5 (((𝐹𝑋) ∈ 𝒫 𝐴 ∧ (𝐹‘(𝐹𝑋)) ⊆ (𝐹𝑋)) → {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤} ⊆ (𝐹𝑋))
6752, 62, 66syl2anc 585 . . . 4 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤} ⊆ (𝐹𝑋))
6838, 67eqsstrid 4031 . . 3 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → 𝑋 ⊆ (𝐹𝑋))
6939, 68eqssd 4000 . 2 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) = 𝑋)
7010, 69jca 513 1 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝑋𝐴 ∧ (𝐹𝑋) = 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088   = wceq 1542  wcel 2107  wral 3062  {crab 3433  wss 3949  𝒫 cpw 4603   cint 4951  cfv 6544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-br 5150  df-iota 6496  df-fv 6552
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator