This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ∩ { 𝑧 ∈ 𝒫 𝐴 ∣ ( 𝐹 ‘ 𝑧 ) ⊆ 𝑧 }
Assertion knatar ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ( 𝑋 ⊆ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑋 ) )

Proof

Step Hyp Ref Expression
1 knatar.1 ⊢ 𝑋 = ∩ { 𝑧 ∈ 𝒫 𝐴 ∣ ( 𝐹 ‘ 𝑧 ) ⊆ 𝑧 }
2 pwidg ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴 )
3 2 3ad2ant1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → 𝐴 ∈ 𝒫 𝐴 )
4 simp2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 )
5 fveq2 ⊢ ( 𝑧 = 𝐴 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝐴 ) )
6 id ⊢ ( 𝑧 = 𝐴 → 𝑧 = 𝐴 )
7 5 6 sseq12d ⊢ ( 𝑧 = 𝐴 → ( ( 𝐹 ‘ 𝑧 ) ⊆ 𝑧 ↔ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ) )
8 7 intminss ⊢ ( ( 𝐴 ∈ 𝒫 𝐴 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ) → ∩ { 𝑧 ∈ 𝒫 𝐴 ∣ ( 𝐹 ‘ 𝑧 ) ⊆ 𝑧 } ⊆ 𝐴 )
9 3 4 8 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ∩ { 𝑧 ∈ 𝒫 𝐴 ∣ ( 𝐹 ‘ 𝑧 ) ⊆ 𝑧 } ⊆ 𝐴 )
10 1 9 eqsstrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → 𝑋 ⊆ 𝐴 )
11 fveq2 ⊢ ( 𝑦 = 𝑋 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) )
12 11 sseq1d ⊢ ( 𝑦 = 𝑋 → ( ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑋 ) ⊆ ( 𝐹 ‘ 𝑤 ) ) )
13 pweq ⊢ ( 𝑥 = 𝑤 → 𝒫 𝑥 = 𝒫 𝑤 )
14 fveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) )
15 14 sseq2d ⊢ ( 𝑥 = 𝑤 → ( ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑤 ) ) )
16 13 15 raleqbidv ⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝒫 𝑤 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑤 ) ) )
17 simpl3 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝐹 ‘ 𝑤 ) ⊆ 𝑤 ) ) → ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) )
18 simprl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝐹 ‘ 𝑤 ) ⊆ 𝑤 ) ) → 𝑤 ∈ 𝒫 𝐴 )
19 16 17 18 rspcdva ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝐹 ‘ 𝑤 ) ⊆ 𝑤 ) ) → ∀ 𝑦 ∈ 𝒫 𝑤 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑤 ) )
20 fveq2 ⊢ ( 𝑧 = 𝑤 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) )
21 id ⊢ ( 𝑧 = 𝑤 → 𝑧 = 𝑤 )
22 20 21 sseq12d ⊢ ( 𝑧 = 𝑤 → ( ( 𝐹 ‘ 𝑧 ) ⊆ 𝑧 ↔ ( 𝐹 ‘ 𝑤 ) ⊆ 𝑤 ) )
23 22 intminss ⊢ ( ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝐹 ‘ 𝑤 ) ⊆ 𝑤 ) → ∩ { 𝑧 ∈ 𝒫 𝐴 ∣ ( 𝐹 ‘ 𝑧 ) ⊆ 𝑧 } ⊆ 𝑤 )
24 23 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝐹 ‘ 𝑤 ) ⊆ 𝑤 ) ) → ∩ { 𝑧 ∈ 𝒫 𝐴 ∣ ( 𝐹 ‘ 𝑧 ) ⊆ 𝑧 } ⊆ 𝑤 )
25 1 24 eqsstrid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝐹 ‘ 𝑤 ) ⊆ 𝑤 ) ) → 𝑋 ⊆ 𝑤 )
26 vex ⊢ 𝑤 ∈ V
27 26 elpw2 ⊢ ( 𝑋 ∈ 𝒫 𝑤 ↔ 𝑋 ⊆ 𝑤 )
28 25 27 sylibr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝐹 ‘ 𝑤 ) ⊆ 𝑤 ) ) → 𝑋 ∈ 𝒫 𝑤 )
29 12 19 28 rspcdva ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝐹 ‘ 𝑤 ) ⊆ 𝑤 ) ) → ( 𝐹 ‘ 𝑋 ) ⊆ ( 𝐹 ‘ 𝑤 ) )
30 simprr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝐹 ‘ 𝑤 ) ⊆ 𝑤 ) ) → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑤 )
31 29 30 sstrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝐹 ‘ 𝑤 ) ⊆ 𝑤 ) ) → ( 𝐹 ‘ 𝑋 ) ⊆ 𝑤 )
32 31 expr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑤 ∈ 𝒫 𝐴 ) → ( ( 𝐹 ‘ 𝑤 ) ⊆ 𝑤 → ( 𝐹 ‘ 𝑋 ) ⊆ 𝑤 ) )
33 32 ralrimiva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ∀ 𝑤 ∈ 𝒫 𝐴 ( ( 𝐹 ‘ 𝑤 ) ⊆ 𝑤 → ( 𝐹 ‘ 𝑋 ) ⊆ 𝑤 ) )
34 ssintrab ⊢ ( ( 𝐹 ‘ 𝑋 ) ⊆ ∩ { 𝑤 ∈ 𝒫 𝐴 ∣ ( 𝐹 ‘ 𝑤 ) ⊆ 𝑤 } ↔ ∀ 𝑤 ∈ 𝒫 𝐴 ( ( 𝐹 ‘ 𝑤 ) ⊆ 𝑤 → ( 𝐹 ‘ 𝑋 ) ⊆ 𝑤 ) )
35 33 34 sylibr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝑋 ) ⊆ ∩ { 𝑤 ∈ 𝒫 𝐴 ∣ ( 𝐹 ‘ 𝑤 ) ⊆ 𝑤 } )
36 22 cbvrabv ⊢ { 𝑧 ∈ 𝒫 𝐴 ∣ ( 𝐹 ‘ 𝑧 ) ⊆ 𝑧 } = { 𝑤 ∈ 𝒫 𝐴 ∣ ( 𝐹 ‘ 𝑤 ) ⊆ 𝑤 }
37 36 inteqi ⊢ ∩ { 𝑧 ∈ 𝒫 𝐴 ∣ ( 𝐹 ‘ 𝑧 ) ⊆ 𝑧 } = ∩ { 𝑤 ∈ 𝒫 𝐴 ∣ ( 𝐹 ‘ 𝑤 ) ⊆ 𝑤 }
38 1 37 eqtri ⊢ 𝑋 = ∩ { 𝑤 ∈ 𝒫 𝐴 ∣ ( 𝐹 ‘ 𝑤 ) ⊆ 𝑤 }
39 35 38 sseqtrrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝑋 ) ⊆ 𝑋 )
40 11 sseq1d ⊢ ( 𝑦 = 𝑋 → ( ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝐴 ) ↔ ( 𝐹 ‘ 𝑋 ) ⊆ ( 𝐹 ‘ 𝐴 ) ) )
41 pweq ⊢ ( 𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴 )
42 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
43 42 sseq2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝐴 ) ) )
44 41 43 raleqbidv ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝐴 ) ) )
45 simp3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) )
46 44 45 3 rspcdva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝐴 ) )
47 3 10 sselpwd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → 𝑋 ∈ 𝒫 𝐴 )
48 40 46 47 rspcdva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝑋 ) ⊆ ( 𝐹 ‘ 𝐴 ) )
49 48 4 sstrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝑋 ) ⊆ 𝐴 )
50 fvex ⊢ ( 𝐹 ‘ 𝑋 ) ∈ V
51 50 elpw ⊢ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝒫 𝐴 ↔ ( 𝐹 ‘ 𝑋 ) ⊆ 𝐴 )
52 49 51 sylibr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝒫 𝐴 )
53 fveq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑋 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐹 ‘ 𝑋 ) ) )
54 53 sseq1d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑋 ) → ( ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ ( 𝐹 ‘ 𝑋 ) ) ⊆ ( 𝐹 ‘ 𝑋 ) ) )
55 pweq ⊢ ( 𝑥 = 𝑋 → 𝒫 𝑥 = 𝒫 𝑋 )
56 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
57 56 sseq2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑋 ) ) )
58 55 57 raleqbidv ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝒫 𝑋 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑋 ) ) )
59 58 45 47 rspcdva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ∀ 𝑦 ∈ 𝒫 𝑋 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑋 ) )
60 50 elpw ⊢ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝒫 𝑋 ↔ ( 𝐹 ‘ 𝑋 ) ⊆ 𝑋 )
61 39 60 sylibr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝒫 𝑋 )
62 54 59 61 rspcdva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑋 ) ) ⊆ ( 𝐹 ‘ 𝑋 ) )
63 fveq2 ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑋 ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝐹 ‘ 𝑋 ) ) )
64 id ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑋 ) → 𝑤 = ( 𝐹 ‘ 𝑋 ) )
65 63 64 sseq12d ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑋 ) → ( ( 𝐹 ‘ 𝑤 ) ⊆ 𝑤 ↔ ( 𝐹 ‘ ( 𝐹 ‘ 𝑋 ) ) ⊆ ( 𝐹 ‘ 𝑋 ) ) )
66 65 intminss ⊢ ( ( ( 𝐹 ‘ 𝑋 ) ∈ 𝒫 𝐴 ∧ ( 𝐹 ‘ ( 𝐹 ‘ 𝑋 ) ) ⊆ ( 𝐹 ‘ 𝑋 ) ) → ∩ { 𝑤 ∈ 𝒫 𝐴 ∣ ( 𝐹 ‘ 𝑤 ) ⊆ 𝑤 } ⊆ ( 𝐹 ‘ 𝑋 ) )
67 52 62 66 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ∩ { 𝑤 ∈ 𝒫 𝐴 ∣ ( 𝐹 ‘ 𝑤 ) ⊆ 𝑤 } ⊆ ( 𝐹 ‘ 𝑋 ) )
68 38 67 eqsstrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → 𝑋 ⊆ ( 𝐹 ‘ 𝑋 ) )
69 39 68 eqssd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑋 )
70 10 69 jca ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ( 𝑋 ⊆ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑋 ) )