Step | Hyp | Ref
| Expression |
1 | | knatar.1 |
. . 3
⊢ 𝑋 = ∩
{𝑧 ∈ 𝒫 𝐴 ∣ (𝐹‘𝑧) ⊆ 𝑧} |
2 | | pwidg 4121 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴) |
3 | 2 | 3ad2ant1 1075 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → 𝐴 ∈ 𝒫 𝐴) |
4 | | simp2 1055 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → (𝐹‘𝐴) ⊆ 𝐴) |
5 | | fveq2 6103 |
. . . . . 6
⊢ (𝑧 = 𝐴 → (𝐹‘𝑧) = (𝐹‘𝐴)) |
6 | | id 22 |
. . . . . 6
⊢ (𝑧 = 𝐴 → 𝑧 = 𝐴) |
7 | 5, 6 | sseq12d 3597 |
. . . . 5
⊢ (𝑧 = 𝐴 → ((𝐹‘𝑧) ⊆ 𝑧 ↔ (𝐹‘𝐴) ⊆ 𝐴)) |
8 | 7 | intminss 4438 |
. . . 4
⊢ ((𝐴 ∈ 𝒫 𝐴 ∧ (𝐹‘𝐴) ⊆ 𝐴) → ∩ {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹‘𝑧) ⊆ 𝑧} ⊆ 𝐴) |
9 | 3, 4, 8 | syl2anc 691 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → ∩ {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹‘𝑧) ⊆ 𝑧} ⊆ 𝐴) |
10 | 1, 9 | syl5eqss 3612 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → 𝑋 ⊆ 𝐴) |
11 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑤 → (𝐹‘𝑧) = (𝐹‘𝑤)) |
12 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑤 → 𝑧 = 𝑤) |
13 | 11, 12 | sseq12d 3597 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑤 → ((𝐹‘𝑧) ⊆ 𝑧 ↔ (𝐹‘𝑤) ⊆ 𝑤)) |
14 | 13 | intminss 4438 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ 𝒫 𝐴 ∧ (𝐹‘𝑤) ⊆ 𝑤) → ∩ {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹‘𝑧) ⊆ 𝑧} ⊆ 𝑤) |
15 | 14 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹‘𝑤) ⊆ 𝑤)) → ∩ {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹‘𝑧) ⊆ 𝑧} ⊆ 𝑤) |
16 | 1, 15 | syl5eqss 3612 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹‘𝑤) ⊆ 𝑤)) → 𝑋 ⊆ 𝑤) |
17 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑤 ∈ V |
18 | 17 | elpw2 4755 |
. . . . . . . . . 10
⊢ (𝑋 ∈ 𝒫 𝑤 ↔ 𝑋 ⊆ 𝑤) |
19 | 16, 18 | sylibr 223 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹‘𝑤) ⊆ 𝑤)) → 𝑋 ∈ 𝒫 𝑤) |
20 | | simprl 790 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹‘𝑤) ⊆ 𝑤)) → 𝑤 ∈ 𝒫 𝐴) |
21 | | simpl3 1059 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹‘𝑤) ⊆ 𝑤)) → ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) |
22 | | pweq 4111 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → 𝒫 𝑥 = 𝒫 𝑤) |
23 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → (𝐹‘𝑥) = (𝐹‘𝑤)) |
24 | 23 | sseq2d 3596 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → ((𝐹‘𝑦) ⊆ (𝐹‘𝑥) ↔ (𝐹‘𝑦) ⊆ (𝐹‘𝑤))) |
25 | 22, 24 | raleqbidv 3129 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → (∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥) ↔ ∀𝑦 ∈ 𝒫 𝑤(𝐹‘𝑦) ⊆ (𝐹‘𝑤))) |
26 | 25 | rspcv 3278 |
. . . . . . . . . 10
⊢ (𝑤 ∈ 𝒫 𝐴 → (∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥) → ∀𝑦 ∈ 𝒫 𝑤(𝐹‘𝑦) ⊆ (𝐹‘𝑤))) |
27 | 20, 21, 26 | sylc 63 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹‘𝑤) ⊆ 𝑤)) → ∀𝑦 ∈ 𝒫 𝑤(𝐹‘𝑦) ⊆ (𝐹‘𝑤)) |
28 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑋 → (𝐹‘𝑦) = (𝐹‘𝑋)) |
29 | 28 | sseq1d 3595 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑋 → ((𝐹‘𝑦) ⊆ (𝐹‘𝑤) ↔ (𝐹‘𝑋) ⊆ (𝐹‘𝑤))) |
30 | 29 | rspcv 3278 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝒫 𝑤 → (∀𝑦 ∈ 𝒫 𝑤(𝐹‘𝑦) ⊆ (𝐹‘𝑤) → (𝐹‘𝑋) ⊆ (𝐹‘𝑤))) |
31 | 19, 27, 30 | sylc 63 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹‘𝑤) ⊆ 𝑤)) → (𝐹‘𝑋) ⊆ (𝐹‘𝑤)) |
32 | | simprr 792 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹‘𝑤) ⊆ 𝑤)) → (𝐹‘𝑤) ⊆ 𝑤) |
33 | 31, 32 | sstrd 3578 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) ∧ (𝑤 ∈ 𝒫 𝐴 ∧ (𝐹‘𝑤) ⊆ 𝑤)) → (𝐹‘𝑋) ⊆ 𝑤) |
34 | 33 | expr 641 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) ∧ 𝑤 ∈ 𝒫 𝐴) → ((𝐹‘𝑤) ⊆ 𝑤 → (𝐹‘𝑋) ⊆ 𝑤)) |
35 | 34 | ralrimiva 2949 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → ∀𝑤 ∈ 𝒫 𝐴((𝐹‘𝑤) ⊆ 𝑤 → (𝐹‘𝑋) ⊆ 𝑤)) |
36 | | ssintrab 4435 |
. . . . 5
⊢ ((𝐹‘𝑋) ⊆ ∩
{𝑤 ∈ 𝒫 𝐴 ∣ (𝐹‘𝑤) ⊆ 𝑤} ↔ ∀𝑤 ∈ 𝒫 𝐴((𝐹‘𝑤) ⊆ 𝑤 → (𝐹‘𝑋) ⊆ 𝑤)) |
37 | 35, 36 | sylibr 223 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → (𝐹‘𝑋) ⊆ ∩
{𝑤 ∈ 𝒫 𝐴 ∣ (𝐹‘𝑤) ⊆ 𝑤}) |
38 | 13 | cbvrabv 3172 |
. . . . . 6
⊢ {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹‘𝑧) ⊆ 𝑧} = {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹‘𝑤) ⊆ 𝑤} |
39 | 38 | inteqi 4414 |
. . . . 5
⊢ ∩ {𝑧
∈ 𝒫 𝐴 ∣
(𝐹‘𝑧) ⊆ 𝑧} = ∩ {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹‘𝑤) ⊆ 𝑤} |
40 | 1, 39 | eqtri 2632 |
. . . 4
⊢ 𝑋 = ∩
{𝑤 ∈ 𝒫 𝐴 ∣ (𝐹‘𝑤) ⊆ 𝑤} |
41 | 37, 40 | syl6sseqr 3615 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → (𝐹‘𝑋) ⊆ 𝑋) |
42 | | elpw2g 4754 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → (𝑋 ∈ 𝒫 𝐴 ↔ 𝑋 ⊆ 𝐴)) |
43 | 42 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → (𝑋 ∈ 𝒫 𝐴 ↔ 𝑋 ⊆ 𝐴)) |
44 | 10, 43 | mpbird 246 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → 𝑋 ∈ 𝒫 𝐴) |
45 | | simp3 1056 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) |
46 | | pweq 4111 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴) |
47 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) |
48 | 47 | sseq2d 3596 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → ((𝐹‘𝑦) ⊆ (𝐹‘𝑥) ↔ (𝐹‘𝑦) ⊆ (𝐹‘𝐴))) |
49 | 46, 48 | raleqbidv 3129 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥) ↔ ∀𝑦 ∈ 𝒫 𝐴(𝐹‘𝑦) ⊆ (𝐹‘𝐴))) |
50 | 49 | rspcv 3278 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝒫 𝐴 → (∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥) → ∀𝑦 ∈ 𝒫 𝐴(𝐹‘𝑦) ⊆ (𝐹‘𝐴))) |
51 | 3, 45, 50 | sylc 63 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → ∀𝑦 ∈ 𝒫 𝐴(𝐹‘𝑦) ⊆ (𝐹‘𝐴)) |
52 | 28 | sseq1d 3595 |
. . . . . . . . 9
⊢ (𝑦 = 𝑋 → ((𝐹‘𝑦) ⊆ (𝐹‘𝐴) ↔ (𝐹‘𝑋) ⊆ (𝐹‘𝐴))) |
53 | 52 | rspcv 3278 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝒫 𝐴 → (∀𝑦 ∈ 𝒫 𝐴(𝐹‘𝑦) ⊆ (𝐹‘𝐴) → (𝐹‘𝑋) ⊆ (𝐹‘𝐴))) |
54 | 44, 51, 53 | sylc 63 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → (𝐹‘𝑋) ⊆ (𝐹‘𝐴)) |
55 | 54, 4 | sstrd 3578 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → (𝐹‘𝑋) ⊆ 𝐴) |
56 | | fvex 6113 |
. . . . . . 7
⊢ (𝐹‘𝑋) ∈ V |
57 | 56 | elpw 4114 |
. . . . . 6
⊢ ((𝐹‘𝑋) ∈ 𝒫 𝐴 ↔ (𝐹‘𝑋) ⊆ 𝐴) |
58 | 55, 57 | sylibr 223 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → (𝐹‘𝑋) ∈ 𝒫 𝐴) |
59 | 56 | elpw 4114 |
. . . . . . 7
⊢ ((𝐹‘𝑋) ∈ 𝒫 𝑋 ↔ (𝐹‘𝑋) ⊆ 𝑋) |
60 | 41, 59 | sylibr 223 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → (𝐹‘𝑋) ∈ 𝒫 𝑋) |
61 | | pweq 4111 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → 𝒫 𝑥 = 𝒫 𝑋) |
62 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋)) |
63 | 62 | sseq2d 3596 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → ((𝐹‘𝑦) ⊆ (𝐹‘𝑥) ↔ (𝐹‘𝑦) ⊆ (𝐹‘𝑋))) |
64 | 61, 63 | raleqbidv 3129 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥) ↔ ∀𝑦 ∈ 𝒫 𝑋(𝐹‘𝑦) ⊆ (𝐹‘𝑋))) |
65 | 64 | rspcv 3278 |
. . . . . . 7
⊢ (𝑋 ∈ 𝒫 𝐴 → (∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥) → ∀𝑦 ∈ 𝒫 𝑋(𝐹‘𝑦) ⊆ (𝐹‘𝑋))) |
66 | 44, 45, 65 | sylc 63 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → ∀𝑦 ∈ 𝒫 𝑋(𝐹‘𝑦) ⊆ (𝐹‘𝑋)) |
67 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑦 = (𝐹‘𝑋) → (𝐹‘𝑦) = (𝐹‘(𝐹‘𝑋))) |
68 | 67 | sseq1d 3595 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝑋) → ((𝐹‘𝑦) ⊆ (𝐹‘𝑋) ↔ (𝐹‘(𝐹‘𝑋)) ⊆ (𝐹‘𝑋))) |
69 | 68 | rspcv 3278 |
. . . . . 6
⊢ ((𝐹‘𝑋) ∈ 𝒫 𝑋 → (∀𝑦 ∈ 𝒫 𝑋(𝐹‘𝑦) ⊆ (𝐹‘𝑋) → (𝐹‘(𝐹‘𝑋)) ⊆ (𝐹‘𝑋))) |
70 | 60, 66, 69 | sylc 63 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → (𝐹‘(𝐹‘𝑋)) ⊆ (𝐹‘𝑋)) |
71 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑤 = (𝐹‘𝑋) → (𝐹‘𝑤) = (𝐹‘(𝐹‘𝑋))) |
72 | | id 22 |
. . . . . . 7
⊢ (𝑤 = (𝐹‘𝑋) → 𝑤 = (𝐹‘𝑋)) |
73 | 71, 72 | sseq12d 3597 |
. . . . . 6
⊢ (𝑤 = (𝐹‘𝑋) → ((𝐹‘𝑤) ⊆ 𝑤 ↔ (𝐹‘(𝐹‘𝑋)) ⊆ (𝐹‘𝑋))) |
74 | 73 | intminss 4438 |
. . . . 5
⊢ (((𝐹‘𝑋) ∈ 𝒫 𝐴 ∧ (𝐹‘(𝐹‘𝑋)) ⊆ (𝐹‘𝑋)) → ∩
{𝑤 ∈ 𝒫 𝐴 ∣ (𝐹‘𝑤) ⊆ 𝑤} ⊆ (𝐹‘𝑋)) |
75 | 58, 70, 74 | syl2anc 691 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → ∩ {𝑤 ∈ 𝒫 𝐴 ∣ (𝐹‘𝑤) ⊆ 𝑤} ⊆ (𝐹‘𝑋)) |
76 | 40, 75 | syl5eqss 3612 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → 𝑋 ⊆ (𝐹‘𝑋)) |
77 | 41, 76 | eqssd 3585 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → (𝐹‘𝑋) = 𝑋) |
78 | 10, 77 | jca 553 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → (𝑋 ⊆ 𝐴 ∧ (𝐹‘𝑋) = 𝑋)) |