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

Theorem knatar 7099
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 4552 . . . . 5 (𝐴𝑉𝐴 ∈ 𝒫 𝐴)
323ad2ant1 1125 . . . 4 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → 𝐴 ∈ 𝒫 𝐴)
4 simp2 1129 . . . 4 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝐴) ⊆ 𝐴)
5 fveq2 6663 . . . . . 6 (𝑧 = 𝐴 → (𝐹𝑧) = (𝐹𝐴))
6 id 22 . . . . . 6 (𝑧 = 𝐴𝑧 = 𝐴)
75, 6sseq12d 3997 . . . . 5 (𝑧 = 𝐴 → ((𝐹𝑧) ⊆ 𝑧 ↔ (𝐹𝐴) ⊆ 𝐴))
87intminss 4893 . . . 4 ((𝐴 ∈ 𝒫 𝐴 ∧ (𝐹𝐴) ⊆ 𝐴) → {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} ⊆ 𝐴)
93, 4, 8syl2anc 584 . . 3 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} ⊆ 𝐴)
101, 9eqsstrid 4012 . 2 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → 𝑋𝐴)
11 fveq2 6663 . . . . . . . . . 10 (𝑦 = 𝑋 → (𝐹𝑦) = (𝐹𝑋))
1211sseq1d 3995 . . . . . . . . 9 (𝑦 = 𝑋 → ((𝐹𝑦) ⊆ (𝐹𝑤) ↔ (𝐹𝑋) ⊆ (𝐹𝑤)))
13 pweq 4538 . . . . . . . . . . 11 (𝑥 = 𝑤 → 𝒫 𝑥 = 𝒫 𝑤)
14 fveq2 6663 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝐹𝑥) = (𝐹𝑤))
1514sseq2d 3996 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((𝐹𝑦) ⊆ (𝐹𝑥) ↔ (𝐹𝑦) ⊆ (𝐹𝑤)))
1613, 15raleqbidv 3399 . . . . . . . . . 10 (𝑥 = 𝑤 → (∀𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥) ↔ ∀𝑦 ∈ 𝒫 𝑤(𝐹𝑦) ⊆ (𝐹𝑤)))
17 simpl3 1185 . . . . . . . . . 10 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥))
18 simprl 767 . . . . . . . . . 10 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → 𝑤 ∈ 𝒫 𝐴)
1916, 17, 18rspcdva 3622 . . . . . . . . 9 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → ∀𝑦 ∈ 𝒫 𝑤(𝐹𝑦) ⊆ (𝐹𝑤))
20 fveq2 6663 . . . . . . . . . . . . . 14 (𝑧 = 𝑤 → (𝐹𝑧) = (𝐹𝑤))
21 id 22 . . . . . . . . . . . . . 14 (𝑧 = 𝑤𝑧 = 𝑤)
2220, 21sseq12d 3997 . . . . . . . . . . . . 13 (𝑧 = 𝑤 → ((𝐹𝑧) ⊆ 𝑧 ↔ (𝐹𝑤) ⊆ 𝑤))
2322intminss 4893 . . . . . . . . . . . 12 ((𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤) → {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} ⊆ 𝑤)
2423adantl 482 . . . . . . . . . . 11 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} ⊆ 𝑤)
251, 24eqsstrid 4012 . . . . . . . . . 10 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → 𝑋𝑤)
26 vex 3495 . . . . . . . . . . 11 𝑤 ∈ V
2726elpw2 5239 . . . . . . . . . 10 (𝑋 ∈ 𝒫 𝑤𝑋𝑤)
2825, 27sylibr 235 . . . . . . . . 9 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → 𝑋 ∈ 𝒫 𝑤)
2912, 19, 28rspcdva 3622 . . . . . . . 8 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → (𝐹𝑋) ⊆ (𝐹𝑤))
30 simprr 769 . . . . . . . 8 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → (𝐹𝑤) ⊆ 𝑤)
3129, 30sstrd 3974 . . . . . . 7 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → (𝐹𝑋) ⊆ 𝑤)
3231expr 457 . . . . . 6 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ 𝑤 ∈ 𝒫 𝐴) → ((𝐹𝑤) ⊆ 𝑤 → (𝐹𝑋) ⊆ 𝑤))
3332ralrimiva 3179 . . . . 5 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → ∀𝑤 ∈ 𝒫 𝐴((𝐹𝑤) ⊆ 𝑤 → (𝐹𝑋) ⊆ 𝑤))
34 ssintrab 4890 . . . . 5 ((𝐹𝑋) ⊆ {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤} ↔ ∀𝑤 ∈ 𝒫 𝐴((𝐹𝑤) ⊆ 𝑤 → (𝐹𝑋) ⊆ 𝑤))
3533, 34sylibr 235 . . . 4 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ⊆ {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤})
3622cbvrabv 3489 . . . . . 6 {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} = {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤}
3736inteqi 4871 . . . . 5 {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} = {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤}
381, 37eqtri 2841 . . . 4 𝑋 = {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤}
3935, 38sseqtrrdi 4015 . . 3 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ⊆ 𝑋)
4011sseq1d 3995 . . . . . . . 8 (𝑦 = 𝑋 → ((𝐹𝑦) ⊆ (𝐹𝐴) ↔ (𝐹𝑋) ⊆ (𝐹𝐴)))
41 pweq 4538 . . . . . . . . . 10 (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
42 fveq2 6663 . . . . . . . . . . 11 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
4342sseq2d 3996 . . . . . . . . . 10 (𝑥 = 𝐴 → ((𝐹𝑦) ⊆ (𝐹𝑥) ↔ (𝐹𝑦) ⊆ (𝐹𝐴)))
4441, 43raleqbidv 3399 . . . . . . . . 9 (𝑥 = 𝐴 → (∀𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥) ↔ ∀𝑦 ∈ 𝒫 𝐴(𝐹𝑦) ⊆ (𝐹𝐴)))
45 simp3 1130 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥))
4644, 45, 3rspcdva 3622 . . . . . . . 8 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → ∀𝑦 ∈ 𝒫 𝐴(𝐹𝑦) ⊆ (𝐹𝐴))
473, 10sselpwd 5221 . . . . . . . 8 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → 𝑋 ∈ 𝒫 𝐴)
4840, 46, 47rspcdva 3622 . . . . . . 7 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ⊆ (𝐹𝐴))
4948, 4sstrd 3974 . . . . . 6 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ⊆ 𝐴)
50 fvex 6676 . . . . . . 7 (𝐹𝑋) ∈ V
5150elpw 4542 . . . . . 6 ((𝐹𝑋) ∈ 𝒫 𝐴 ↔ (𝐹𝑋) ⊆ 𝐴)
5249, 51sylibr 235 . . . . 5 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ∈ 𝒫 𝐴)
53 fveq2 6663 . . . . . . 7 (𝑦 = (𝐹𝑋) → (𝐹𝑦) = (𝐹‘(𝐹𝑋)))
5453sseq1d 3995 . . . . . 6 (𝑦 = (𝐹𝑋) → ((𝐹𝑦) ⊆ (𝐹𝑋) ↔ (𝐹‘(𝐹𝑋)) ⊆ (𝐹𝑋)))
55 pweq 4538 . . . . . . . 8 (𝑥 = 𝑋 → 𝒫 𝑥 = 𝒫 𝑋)
56 fveq2 6663 . . . . . . . . 9 (𝑥 = 𝑋 → (𝐹𝑥) = (𝐹𝑋))
5756sseq2d 3996 . . . . . . . 8 (𝑥 = 𝑋 → ((𝐹𝑦) ⊆ (𝐹𝑥) ↔ (𝐹𝑦) ⊆ (𝐹𝑋)))
5855, 57raleqbidv 3399 . . . . . . 7 (𝑥 = 𝑋 → (∀𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥) ↔ ∀𝑦 ∈ 𝒫 𝑋(𝐹𝑦) ⊆ (𝐹𝑋)))
5958, 45, 47rspcdva 3622 . . . . . 6 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → ∀𝑦 ∈ 𝒫 𝑋(𝐹𝑦) ⊆ (𝐹𝑋))
6050elpw 4542 . . . . . . 7 ((𝐹𝑋) ∈ 𝒫 𝑋 ↔ (𝐹𝑋) ⊆ 𝑋)
6139, 60sylibr 235 . . . . . 6 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ∈ 𝒫 𝑋)
6254, 59, 61rspcdva 3622 . . . . 5 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹‘(𝐹𝑋)) ⊆ (𝐹𝑋))
63 fveq2 6663 . . . . . . 7 (𝑤 = (𝐹𝑋) → (𝐹𝑤) = (𝐹‘(𝐹𝑋)))
64 id 22 . . . . . . 7 (𝑤 = (𝐹𝑋) → 𝑤 = (𝐹𝑋))
6563, 64sseq12d 3997 . . . . . 6 (𝑤 = (𝐹𝑋) → ((𝐹𝑤) ⊆ 𝑤 ↔ (𝐹‘(𝐹𝑋)) ⊆ (𝐹𝑋)))
6665intminss 4893 . . . . 5 (((𝐹𝑋) ∈ 𝒫 𝐴 ∧ (𝐹‘(𝐹𝑋)) ⊆ (𝐹𝑋)) → {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤} ⊆ (𝐹𝑋))
6752, 62, 66syl2anc 584 . . . 4 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤} ⊆ (𝐹𝑋))
6838, 67eqsstrid 4012 . . 3 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → 𝑋 ⊆ (𝐹𝑋))
6939, 68eqssd 3981 . 2 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) = 𝑋)
7010, 69jca 512 1 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝑋𝐴 ∧ (𝐹𝑋) = 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079   = wceq 1528  wcel 2105  wral 3135  {crab 3139  wss 3933  𝒫 cpw 4535   cint 4867  cfv 6348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-int 4868  df-br 5058  df-iota 6307  df-fv 6356
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator