| Step | Hyp | Ref
| Expression |
| 1 | | fpwwe2.1 |
. . . . . 6
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} |
| 2 | 1 | relopabiv 5830 |
. . . . 5
⊢ Rel 𝑊 |
| 3 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → Rel 𝑊) |
| 4 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑤𝑊𝑠 ∧ 𝑤𝑊𝑡)) ∧ (𝑤 ⊆ 𝑤 ∧ 𝑠 = (𝑡 ∩ (𝑤 × 𝑤)))) → 𝑠 = (𝑡 ∩ (𝑤 × 𝑤))) |
| 5 | | fpwwe2.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 6 | 1, 5 | fpwwe2lem2 10672 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑤𝑊𝑡 ↔ ((𝑤 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑤 × 𝑤)) ∧ (𝑡 We 𝑤 ∧ ∀𝑦 ∈ 𝑤 [(◡𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦)))) |
| 7 | 6 | simprbda 498 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤𝑊𝑡) → (𝑤 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑤 × 𝑤))) |
| 8 | 7 | simprd 495 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤𝑊𝑡) → 𝑡 ⊆ (𝑤 × 𝑤)) |
| 9 | 8 | adantrl 716 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑤𝑊𝑠 ∧ 𝑤𝑊𝑡)) → 𝑡 ⊆ (𝑤 × 𝑤)) |
| 10 | 9 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑤𝑊𝑠 ∧ 𝑤𝑊𝑡)) ∧ (𝑤 ⊆ 𝑤 ∧ 𝑠 = (𝑡 ∩ (𝑤 × 𝑤)))) → 𝑡 ⊆ (𝑤 × 𝑤)) |
| 11 | | dfss2 3969 |
. . . . . . . . . 10
⊢ (𝑡 ⊆ (𝑤 × 𝑤) ↔ (𝑡 ∩ (𝑤 × 𝑤)) = 𝑡) |
| 12 | 10, 11 | sylib 218 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑤𝑊𝑠 ∧ 𝑤𝑊𝑡)) ∧ (𝑤 ⊆ 𝑤 ∧ 𝑠 = (𝑡 ∩ (𝑤 × 𝑤)))) → (𝑡 ∩ (𝑤 × 𝑤)) = 𝑡) |
| 13 | 4, 12 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑤𝑊𝑠 ∧ 𝑤𝑊𝑡)) ∧ (𝑤 ⊆ 𝑤 ∧ 𝑠 = (𝑡 ∩ (𝑤 × 𝑤)))) → 𝑠 = 𝑡) |
| 14 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑤𝑊𝑠 ∧ 𝑤𝑊𝑡)) ∧ (𝑤 ⊆ 𝑤 ∧ 𝑡 = (𝑠 ∩ (𝑤 × 𝑤)))) → 𝑡 = (𝑠 ∩ (𝑤 × 𝑤))) |
| 15 | 1, 5 | fpwwe2lem2 10672 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑤𝑊𝑠 ↔ ((𝑤 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑤 × 𝑤)) ∧ (𝑠 We 𝑤 ∧ ∀𝑦 ∈ 𝑤 [(◡𝑠 “ {𝑦}) / 𝑢](𝑢𝐹(𝑠 ∩ (𝑢 × 𝑢))) = 𝑦)))) |
| 16 | 15 | simprbda 498 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤𝑊𝑠) → (𝑤 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑤 × 𝑤))) |
| 17 | 16 | simprd 495 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤𝑊𝑠) → 𝑠 ⊆ (𝑤 × 𝑤)) |
| 18 | 17 | adantrr 717 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑤𝑊𝑠 ∧ 𝑤𝑊𝑡)) → 𝑠 ⊆ (𝑤 × 𝑤)) |
| 19 | 18 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑤𝑊𝑠 ∧ 𝑤𝑊𝑡)) ∧ (𝑤 ⊆ 𝑤 ∧ 𝑡 = (𝑠 ∩ (𝑤 × 𝑤)))) → 𝑠 ⊆ (𝑤 × 𝑤)) |
| 20 | | dfss2 3969 |
. . . . . . . . . 10
⊢ (𝑠 ⊆ (𝑤 × 𝑤) ↔ (𝑠 ∩ (𝑤 × 𝑤)) = 𝑠) |
| 21 | 19, 20 | sylib 218 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑤𝑊𝑠 ∧ 𝑤𝑊𝑡)) ∧ (𝑤 ⊆ 𝑤 ∧ 𝑡 = (𝑠 ∩ (𝑤 × 𝑤)))) → (𝑠 ∩ (𝑤 × 𝑤)) = 𝑠) |
| 22 | 14, 21 | eqtr2d 2778 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑤𝑊𝑠 ∧ 𝑤𝑊𝑡)) ∧ (𝑤 ⊆ 𝑤 ∧ 𝑡 = (𝑠 ∩ (𝑤 × 𝑤)))) → 𝑠 = 𝑡) |
| 23 | 5 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑤𝑊𝑠 ∧ 𝑤𝑊𝑡)) → 𝐴 ∈ 𝑉) |
| 24 | | fpwwe2.3 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) |
| 25 | 24 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑤𝑊𝑠 ∧ 𝑤𝑊𝑡)) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) |
| 26 | | simprl 771 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑤𝑊𝑠 ∧ 𝑤𝑊𝑡)) → 𝑤𝑊𝑠) |
| 27 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑤𝑊𝑠 ∧ 𝑤𝑊𝑡)) → 𝑤𝑊𝑡) |
| 28 | 1, 23, 25, 26, 27 | fpwwe2lem9 10679 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑤𝑊𝑠 ∧ 𝑤𝑊𝑡)) → ((𝑤 ⊆ 𝑤 ∧ 𝑠 = (𝑡 ∩ (𝑤 × 𝑤))) ∨ (𝑤 ⊆ 𝑤 ∧ 𝑡 = (𝑠 ∩ (𝑤 × 𝑤))))) |
| 29 | 13, 22, 28 | mpjaodan 961 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑤𝑊𝑠 ∧ 𝑤𝑊𝑡)) → 𝑠 = 𝑡) |
| 30 | 29 | ex 412 |
. . . . . 6
⊢ (𝜑 → ((𝑤𝑊𝑠 ∧ 𝑤𝑊𝑡) → 𝑠 = 𝑡)) |
| 31 | 30 | alrimiv 1927 |
. . . . 5
⊢ (𝜑 → ∀𝑡((𝑤𝑊𝑠 ∧ 𝑤𝑊𝑡) → 𝑠 = 𝑡)) |
| 32 | 31 | alrimivv 1928 |
. . . 4
⊢ (𝜑 → ∀𝑤∀𝑠∀𝑡((𝑤𝑊𝑠 ∧ 𝑤𝑊𝑡) → 𝑠 = 𝑡)) |
| 33 | | dffun2 6571 |
. . . 4
⊢ (Fun
𝑊 ↔ (Rel 𝑊 ∧ ∀𝑤∀𝑠∀𝑡((𝑤𝑊𝑠 ∧ 𝑤𝑊𝑡) → 𝑠 = 𝑡))) |
| 34 | 3, 32, 33 | sylanbrc 583 |
. . 3
⊢ (𝜑 → Fun 𝑊) |
| 35 | 34 | funfnd 6597 |
. 2
⊢ (𝜑 → 𝑊 Fn dom 𝑊) |
| 36 | | vex 3484 |
. . . . 5
⊢ 𝑠 ∈ V |
| 37 | 36 | elrn 5904 |
. . . 4
⊢ (𝑠 ∈ ran 𝑊 ↔ ∃𝑤 𝑤𝑊𝑠) |
| 38 | 2 | releldmi 5959 |
. . . . . . . . . . . 12
⊢ (𝑤𝑊𝑠 → 𝑤 ∈ dom 𝑊) |
| 39 | 38 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤𝑊𝑠) → 𝑤 ∈ dom 𝑊) |
| 40 | | elssuni 4937 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ dom 𝑊 → 𝑤 ⊆ ∪ dom
𝑊) |
| 41 | 39, 40 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤𝑊𝑠) → 𝑤 ⊆ ∪ dom
𝑊) |
| 42 | | fpwwe2.4 |
. . . . . . . . . 10
⊢ 𝑋 = ∪
dom 𝑊 |
| 43 | 41, 42 | sseqtrrdi 4025 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤𝑊𝑠) → 𝑤 ⊆ 𝑋) |
| 44 | | xpss12 5700 |
. . . . . . . . 9
⊢ ((𝑤 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑋) → (𝑤 × 𝑤) ⊆ (𝑋 × 𝑋)) |
| 45 | 43, 43, 44 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤𝑊𝑠) → (𝑤 × 𝑤) ⊆ (𝑋 × 𝑋)) |
| 46 | 17, 45 | sstrd 3994 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤𝑊𝑠) → 𝑠 ⊆ (𝑋 × 𝑋)) |
| 47 | 46 | ex 412 |
. . . . . 6
⊢ (𝜑 → (𝑤𝑊𝑠 → 𝑠 ⊆ (𝑋 × 𝑋))) |
| 48 | | velpw 4605 |
. . . . . 6
⊢ (𝑠 ∈ 𝒫 (𝑋 × 𝑋) ↔ 𝑠 ⊆ (𝑋 × 𝑋)) |
| 49 | 47, 48 | imbitrrdi 252 |
. . . . 5
⊢ (𝜑 → (𝑤𝑊𝑠 → 𝑠 ∈ 𝒫 (𝑋 × 𝑋))) |
| 50 | 49 | exlimdv 1933 |
. . . 4
⊢ (𝜑 → (∃𝑤 𝑤𝑊𝑠 → 𝑠 ∈ 𝒫 (𝑋 × 𝑋))) |
| 51 | 37, 50 | biimtrid 242 |
. . 3
⊢ (𝜑 → (𝑠 ∈ ran 𝑊 → 𝑠 ∈ 𝒫 (𝑋 × 𝑋))) |
| 52 | 51 | ssrdv 3989 |
. 2
⊢ (𝜑 → ran 𝑊 ⊆ 𝒫 (𝑋 × 𝑋)) |
| 53 | | df-f 6565 |
. 2
⊢ (𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋) ↔ (𝑊 Fn dom 𝑊 ∧ ran 𝑊 ⊆ 𝒫 (𝑋 × 𝑋))) |
| 54 | 35, 52, 53 | sylanbrc 583 |
1
⊢ (𝜑 → 𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋)) |