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

Theorem knatar 6750
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 4312 . . . . 5 (𝐴𝑉𝐴 ∈ 𝒫 𝐴)
323ad2ant1 1127 . . . 4 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → 𝐴 ∈ 𝒫 𝐴)
4 simp2 1131 . . . 4 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝐴) ⊆ 𝐴)
5 fveq2 6332 . . . . . 6 (𝑧 = 𝐴 → (𝐹𝑧) = (𝐹𝐴))
6 id 22 . . . . . 6 (𝑧 = 𝐴𝑧 = 𝐴)
75, 6sseq12d 3783 . . . . 5 (𝑧 = 𝐴 → ((𝐹𝑧) ⊆ 𝑧 ↔ (𝐹𝐴) ⊆ 𝐴))
87intminss 4637 . . . 4 ((𝐴 ∈ 𝒫 𝐴 ∧ (𝐹𝐴) ⊆ 𝐴) → {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} ⊆ 𝐴)
93, 4, 8syl2anc 573 . . 3 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} ⊆ 𝐴)
101, 9syl5eqss 3798 . 2 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → 𝑋𝐴)
11 fveq2 6332 . . . . . . . . . 10 (𝑦 = 𝑋 → (𝐹𝑦) = (𝐹𝑋))
1211sseq1d 3781 . . . . . . . . 9 (𝑦 = 𝑋 → ((𝐹𝑦) ⊆ (𝐹𝑤) ↔ (𝐹𝑋) ⊆ (𝐹𝑤)))
13 pweq 4300 . . . . . . . . . . 11 (𝑥 = 𝑤 → 𝒫 𝑥 = 𝒫 𝑤)
14 fveq2 6332 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝐹𝑥) = (𝐹𝑤))
1514sseq2d 3782 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((𝐹𝑦) ⊆ (𝐹𝑥) ↔ (𝐹𝑦) ⊆ (𝐹𝑤)))
1613, 15raleqbidv 3301 . . . . . . . . . 10 (𝑥 = 𝑤 → (∀𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥) ↔ ∀𝑦 ∈ 𝒫 𝑤(𝐹𝑦) ⊆ (𝐹𝑤)))
17 simpl3 1231 . . . . . . . . . 10 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥))
18 simprl 754 . . . . . . . . . 10 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → 𝑤 ∈ 𝒫 𝐴)
1916, 17, 18rspcdva 3466 . . . . . . . . 9 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → ∀𝑦 ∈ 𝒫 𝑤(𝐹𝑦) ⊆ (𝐹𝑤))
20 fveq2 6332 . . . . . . . . . . . . . 14 (𝑧 = 𝑤 → (𝐹𝑧) = (𝐹𝑤))
21 id 22 . . . . . . . . . . . . . 14 (𝑧 = 𝑤𝑧 = 𝑤)
2220, 21sseq12d 3783 . . . . . . . . . . . . 13 (𝑧 = 𝑤 → ((𝐹𝑧) ⊆ 𝑧 ↔ (𝐹𝑤) ⊆ 𝑤))
2322intminss 4637 . . . . . . . . . . . 12 ((𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤) → {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} ⊆ 𝑤)
2423adantl 467 . . . . . . . . . . 11 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} ⊆ 𝑤)
251, 24syl5eqss 3798 . . . . . . . . . 10 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → 𝑋𝑤)
26 vex 3354 . . . . . . . . . . 11 𝑤 ∈ V
2726elpw2 4959 . . . . . . . . . 10 (𝑋 ∈ 𝒫 𝑤𝑋𝑤)
2825, 27sylibr 224 . . . . . . . . 9 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → 𝑋 ∈ 𝒫 𝑤)
2912, 19, 28rspcdva 3466 . . . . . . . 8 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → (𝐹𝑋) ⊆ (𝐹𝑤))
30 simprr 756 . . . . . . . 8 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → (𝐹𝑤) ⊆ 𝑤)
3129, 30sstrd 3762 . . . . . . 7 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹𝑤) ⊆ 𝑤)) → (𝐹𝑋) ⊆ 𝑤)
3231expr 444 . . . . . 6 (((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) ∧ 𝑤 ∈ 𝒫 𝐴) → ((𝐹𝑤) ⊆ 𝑤 → (𝐹𝑋) ⊆ 𝑤))
3332ralrimiva 3115 . . . . 5 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → ∀𝑤 ∈ 𝒫 𝐴((𝐹𝑤) ⊆ 𝑤 → (𝐹𝑋) ⊆ 𝑤))
34 ssintrab 4634 . . . . 5 ((𝐹𝑋) ⊆ {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤} ↔ ∀𝑤 ∈ 𝒫 𝐴((𝐹𝑤) ⊆ 𝑤 → (𝐹𝑋) ⊆ 𝑤))
3533, 34sylibr 224 . . . 4 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ⊆ {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤})
3622cbvrabv 3349 . . . . . 6 {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} = {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤}
3736inteqi 4615 . . . . 5 {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹𝑧) ⊆ 𝑧} = {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤}
381, 37eqtri 2793 . . . 4 𝑋 = {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤}
3935, 38syl6sseqr 3801 . . 3 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ⊆ 𝑋)
4011sseq1d 3781 . . . . . . . 8 (𝑦 = 𝑋 → ((𝐹𝑦) ⊆ (𝐹𝐴) ↔ (𝐹𝑋) ⊆ (𝐹𝐴)))
41 pweq 4300 . . . . . . . . . 10 (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
42 fveq2 6332 . . . . . . . . . . 11 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
4342sseq2d 3782 . . . . . . . . . 10 (𝑥 = 𝐴 → ((𝐹𝑦) ⊆ (𝐹𝑥) ↔ (𝐹𝑦) ⊆ (𝐹𝐴)))
4441, 43raleqbidv 3301 . . . . . . . . 9 (𝑥 = 𝐴 → (∀𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥) ↔ ∀𝑦 ∈ 𝒫 𝐴(𝐹𝑦) ⊆ (𝐹𝐴)))
45 simp3 1132 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥))
4644, 45, 3rspcdva 3466 . . . . . . . 8 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → ∀𝑦 ∈ 𝒫 𝐴(𝐹𝑦) ⊆ (𝐹𝐴))
473, 10sselpwd 4941 . . . . . . . 8 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → 𝑋 ∈ 𝒫 𝐴)
4840, 46, 47rspcdva 3466 . . . . . . 7 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ⊆ (𝐹𝐴))
4948, 4sstrd 3762 . . . . . 6 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ⊆ 𝐴)
50 fvex 6342 . . . . . . 7 (𝐹𝑋) ∈ V
5150elpw 4303 . . . . . 6 ((𝐹𝑋) ∈ 𝒫 𝐴 ↔ (𝐹𝑋) ⊆ 𝐴)
5249, 51sylibr 224 . . . . 5 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ∈ 𝒫 𝐴)
53 fveq2 6332 . . . . . . 7 (𝑦 = (𝐹𝑋) → (𝐹𝑦) = (𝐹‘(𝐹𝑋)))
5453sseq1d 3781 . . . . . 6 (𝑦 = (𝐹𝑋) → ((𝐹𝑦) ⊆ (𝐹𝑋) ↔ (𝐹‘(𝐹𝑋)) ⊆ (𝐹𝑋)))
55 pweq 4300 . . . . . . . 8 (𝑥 = 𝑋 → 𝒫 𝑥 = 𝒫 𝑋)
56 fveq2 6332 . . . . . . . . 9 (𝑥 = 𝑋 → (𝐹𝑥) = (𝐹𝑋))
5756sseq2d 3782 . . . . . . . 8 (𝑥 = 𝑋 → ((𝐹𝑦) ⊆ (𝐹𝑥) ↔ (𝐹𝑦) ⊆ (𝐹𝑋)))
5855, 57raleqbidv 3301 . . . . . . 7 (𝑥 = 𝑋 → (∀𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥) ↔ ∀𝑦 ∈ 𝒫 𝑋(𝐹𝑦) ⊆ (𝐹𝑋)))
5958, 45, 47rspcdva 3466 . . . . . 6 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → ∀𝑦 ∈ 𝒫 𝑋(𝐹𝑦) ⊆ (𝐹𝑋))
6050elpw 4303 . . . . . . 7 ((𝐹𝑋) ∈ 𝒫 𝑋 ↔ (𝐹𝑋) ⊆ 𝑋)
6139, 60sylibr 224 . . . . . 6 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) ∈ 𝒫 𝑋)
6254, 59, 61rspcdva 3466 . . . . 5 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹‘(𝐹𝑋)) ⊆ (𝐹𝑋))
63 fveq2 6332 . . . . . . 7 (𝑤 = (𝐹𝑋) → (𝐹𝑤) = (𝐹‘(𝐹𝑋)))
64 id 22 . . . . . . 7 (𝑤 = (𝐹𝑋) → 𝑤 = (𝐹𝑋))
6563, 64sseq12d 3783 . . . . . 6 (𝑤 = (𝐹𝑋) → ((𝐹𝑤) ⊆ 𝑤 ↔ (𝐹‘(𝐹𝑋)) ⊆ (𝐹𝑋)))
6665intminss 4637 . . . . 5 (((𝐹𝑋) ∈ 𝒫 𝐴 ∧ (𝐹‘(𝐹𝑋)) ⊆ (𝐹𝑋)) → {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤} ⊆ (𝐹𝑋))
6752, 62, 66syl2anc 573 . . . 4 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹𝑤) ⊆ 𝑤} ⊆ (𝐹𝑋))
6838, 67syl5eqss 3798 . . 3 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → 𝑋 ⊆ (𝐹𝑋))
6939, 68eqssd 3769 . 2 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝐹𝑋) = 𝑋)
7010, 69jca 501 1 ((𝐴𝑉 ∧ (𝐹𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝑥(𝐹𝑦) ⊆ (𝐹𝑥)) → (𝑋𝐴 ∧ (𝐹𝑋) = 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071   = wceq 1631  wcel 2145  wral 3061  {crab 3065  wss 3723  𝒫 cpw 4297   cint 4611  cfv 6031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-int 4612  df-br 4787  df-iota 5994  df-fv 6039
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator