Step | Hyp | Ref
| Expression |
1 | | fpwwe2.4 |
. . . . 5
⊢ 𝑋 = ∪
dom 𝑊 |
2 | | vex 3412 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
3 | 2 | eldm 5769 |
. . . . . . . 8
⊢ (𝑎 ∈ dom 𝑊 ↔ ∃𝑠 𝑎𝑊𝑠) |
4 | | fpwwe2.1 |
. . . . . . . . . . . . . 14
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} |
5 | | fpwwe2.2 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
6 | 4, 5 | fpwwe2lem2 10246 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑎𝑊𝑠 ↔ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑦 ∈ 𝑎 [(◡𝑠 “ {𝑦}) / 𝑢](𝑢𝐹(𝑠 ∩ (𝑢 × 𝑢))) = 𝑦)))) |
7 | 6 | simprbda 502 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎))) |
8 | 7 | simpld 498 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ⊆ 𝐴) |
9 | | velpw 4518 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ 𝒫 𝐴 ↔ 𝑎 ⊆ 𝐴) |
10 | 8, 9 | sylibr 237 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ∈ 𝒫 𝐴) |
11 | 10 | ex 416 |
. . . . . . . . 9
⊢ (𝜑 → (𝑎𝑊𝑠 → 𝑎 ∈ 𝒫 𝐴)) |
12 | 11 | exlimdv 1941 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑠 𝑎𝑊𝑠 → 𝑎 ∈ 𝒫 𝐴)) |
13 | 3, 12 | syl5bi 245 |
. . . . . . 7
⊢ (𝜑 → (𝑎 ∈ dom 𝑊 → 𝑎 ∈ 𝒫 𝐴)) |
14 | 13 | ssrdv 3907 |
. . . . . 6
⊢ (𝜑 → dom 𝑊 ⊆ 𝒫 𝐴) |
15 | | sspwuni 5008 |
. . . . . 6
⊢ (dom
𝑊 ⊆ 𝒫 𝐴 ↔ ∪ dom 𝑊 ⊆ 𝐴) |
16 | 14, 15 | sylib 221 |
. . . . 5
⊢ (𝜑 → ∪ dom 𝑊 ⊆ 𝐴) |
17 | 1, 16 | eqsstrid 3949 |
. . . 4
⊢ (𝜑 → 𝑋 ⊆ 𝐴) |
18 | | vex 3412 |
. . . . . . . 8
⊢ 𝑠 ∈ V |
19 | 18 | elrn 5762 |
. . . . . . 7
⊢ (𝑠 ∈ ran 𝑊 ↔ ∃𝑎 𝑎𝑊𝑠) |
20 | 7 | simprd 499 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑠 ⊆ (𝑎 × 𝑎)) |
21 | 4 | relopabiv 5690 |
. . . . . . . . . . . . . . . 16
⊢ Rel 𝑊 |
22 | 21 | releldmi 5817 |
. . . . . . . . . . . . . . 15
⊢ (𝑎𝑊𝑠 → 𝑎 ∈ dom 𝑊) |
23 | 22 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ∈ dom 𝑊) |
24 | | elssuni 4851 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ dom 𝑊 → 𝑎 ⊆ ∪ dom
𝑊) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ⊆ ∪ dom
𝑊) |
26 | 25, 1 | sseqtrrdi 3952 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ⊆ 𝑋) |
27 | | xpss12 5566 |
. . . . . . . . . . . 12
⊢ ((𝑎 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑋) → (𝑎 × 𝑎) ⊆ (𝑋 × 𝑋)) |
28 | 26, 26, 27 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑎 × 𝑎) ⊆ (𝑋 × 𝑋)) |
29 | 20, 28 | sstrd 3911 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑠 ⊆ (𝑋 × 𝑋)) |
30 | | velpw 4518 |
. . . . . . . . . 10
⊢ (𝑠 ∈ 𝒫 (𝑋 × 𝑋) ↔ 𝑠 ⊆ (𝑋 × 𝑋)) |
31 | 29, 30 | sylibr 237 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑠 ∈ 𝒫 (𝑋 × 𝑋)) |
32 | 31 | ex 416 |
. . . . . . . 8
⊢ (𝜑 → (𝑎𝑊𝑠 → 𝑠 ∈ 𝒫 (𝑋 × 𝑋))) |
33 | 32 | exlimdv 1941 |
. . . . . . 7
⊢ (𝜑 → (∃𝑎 𝑎𝑊𝑠 → 𝑠 ∈ 𝒫 (𝑋 × 𝑋))) |
34 | 19, 33 | syl5bi 245 |
. . . . . 6
⊢ (𝜑 → (𝑠 ∈ ran 𝑊 → 𝑠 ∈ 𝒫 (𝑋 × 𝑋))) |
35 | 34 | ssrdv 3907 |
. . . . 5
⊢ (𝜑 → ran 𝑊 ⊆ 𝒫 (𝑋 × 𝑋)) |
36 | | sspwuni 5008 |
. . . . 5
⊢ (ran
𝑊 ⊆ 𝒫 (𝑋 × 𝑋) ↔ ∪ ran
𝑊 ⊆ (𝑋 × 𝑋)) |
37 | 35, 36 | sylib 221 |
. . . 4
⊢ (𝜑 → ∪ ran 𝑊 ⊆ (𝑋 × 𝑋)) |
38 | 17, 37 | jca 515 |
. . 3
⊢ (𝜑 → (𝑋 ⊆ 𝐴 ∧ ∪ ran
𝑊 ⊆ (𝑋 × 𝑋))) |
39 | | n0 4261 |
. . . . . . . . 9
⊢ (𝑛 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝑛) |
40 | | ssel2 3895 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛) → 𝑦 ∈ 𝑋) |
41 | 40 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → 𝑦 ∈ 𝑋) |
42 | 1 | eleq2i 2829 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝑋 ↔ 𝑦 ∈ ∪ dom
𝑊) |
43 | | eluni2 4823 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ∪ dom 𝑊 ↔ ∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎) |
44 | 42, 43 | bitri 278 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑋 ↔ ∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎) |
45 | 41, 44 | sylib 221 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → ∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎) |
46 | 2 | inex2 5211 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∩ 𝑎) ∈ V |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑛 ∩ 𝑎) ∈ V) |
48 | 6 | simplbda 503 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑠 We 𝑎 ∧ ∀𝑦 ∈ 𝑎 [(◡𝑠 “ {𝑦}) / 𝑢](𝑢𝐹(𝑠 ∩ (𝑢 × 𝑢))) = 𝑦)) |
49 | 48 | simpld 498 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑠 We 𝑎) |
50 | 49 | ad2ant2r 747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑠 We 𝑎) |
51 | | wefr 5541 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 We 𝑎 → 𝑠 Fr 𝑎) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑠 Fr 𝑎) |
53 | | inss2 4144 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∩ 𝑎) ⊆ 𝑎 |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑛 ∩ 𝑎) ⊆ 𝑎) |
55 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑦 ∈ 𝑛) |
56 | | simprr 773 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑦 ∈ 𝑎) |
57 | | inelcm 4379 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ 𝑛 ∧ 𝑦 ∈ 𝑎) → (𝑛 ∩ 𝑎) ≠ ∅) |
58 | 55, 56, 57 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑛 ∩ 𝑎) ≠ ∅) |
59 | | fri 5512 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑛 ∩ 𝑎) ∈ V ∧ 𝑠 Fr 𝑎) ∧ ((𝑛 ∩ 𝑎) ⊆ 𝑎 ∧ (𝑛 ∩ 𝑎) ≠ ∅)) → ∃𝑣 ∈ (𝑛 ∩ 𝑎)∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣) |
60 | 47, 52, 54, 58, 59 | syl22anc 839 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ∃𝑣 ∈ (𝑛 ∩ 𝑎)∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣) |
61 | | simprl 771 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣 ∈ (𝑛 ∩ 𝑎)) |
62 | 61 | elin1d 4112 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣 ∈ 𝑛) |
63 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣) |
64 | | ralnex 3158 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑧 ∈
(𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣 ↔ ¬ ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣) |
65 | 63, 64 | sylib 221 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → ¬ ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣) |
66 | | df-br 5054 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤∪ ran
𝑊 𝑣 ↔ 〈𝑤, 𝑣〉 ∈ ∪
ran 𝑊) |
67 | | eluni2 4823 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(〈𝑤, 𝑣〉 ∈ ∪ ran 𝑊 ↔ ∃𝑡 ∈ ran 𝑊〈𝑤, 𝑣〉 ∈ 𝑡) |
68 | 66, 67 | bitri 278 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤∪ ran
𝑊 𝑣 ↔ ∃𝑡 ∈ ran 𝑊〈𝑤, 𝑣〉 ∈ 𝑡) |
69 | | vex 3412 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑡 ∈ V |
70 | 69 | elrn 5762 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 ∈ ran 𝑊 ↔ ∃𝑏 𝑏𝑊𝑡) |
71 | | df-br 5054 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤𝑡𝑣 ↔ 〈𝑤, 𝑣〉 ∈ 𝑡) |
72 | | simprll 779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤 ∈ 𝑛) |
73 | 72 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑛) |
74 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤𝑡𝑣) |
75 | | simp-4l 783 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝜑) |
76 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑎𝑊𝑠) |
77 | 76 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑎𝑊𝑠) |
78 | | simprlr 780 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑏𝑊𝑡) |
79 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑏𝑊𝑡) |
80 | 4, 5 | fpwwe2lem2 10246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝜑 → (𝑏𝑊𝑡 ↔ ((𝑏 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦 ∈ 𝑏 [(◡𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦)))) |
81 | 80 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → (𝑏𝑊𝑡 ↔ ((𝑏 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦 ∈ 𝑏 [(◡𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦)))) |
82 | 79, 81 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → ((𝑏 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦 ∈ 𝑏 [(◡𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))) |
83 | 82 | simpld 498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → (𝑏 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑏 × 𝑏))) |
84 | 83 | simprd 499 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑡 ⊆ (𝑏 × 𝑏)) |
85 | 75, 77, 78, 84 | syl12anc 837 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑡 ⊆ (𝑏 × 𝑏)) |
86 | 85 | ssbrd 5096 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → (𝑤𝑡𝑣 → 𝑤(𝑏 × 𝑏)𝑣)) |
87 | 74, 86 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤(𝑏 × 𝑏)𝑣) |
88 | | brxp 5598 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑤(𝑏 × 𝑏)𝑣 ↔ (𝑤 ∈ 𝑏 ∧ 𝑣 ∈ 𝑏)) |
89 | 88 | simplbi 501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑤(𝑏 × 𝑏)𝑣 → 𝑤 ∈ 𝑏) |
90 | 87, 89 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤 ∈ 𝑏) |
91 | 90 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑏) |
92 | 61 | elin2d 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣 ∈ 𝑎) |
93 | 92 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑣 ∈ 𝑎) |
94 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑡𝑣) |
95 | | brinxp2 5626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣 ↔ ((𝑤 ∈ 𝑏 ∧ 𝑣 ∈ 𝑎) ∧ 𝑤𝑡𝑣)) |
96 | 91, 93, 94, 95 | syl21anbrc 1346 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣) |
97 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) |
98 | 97 | breqd 5064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑠𝑣 ↔ 𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣)) |
99 | 96, 98 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑠𝑣) |
100 | 75, 77, 20 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑠 ⊆ (𝑎 × 𝑎)) |
101 | 100 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 ⊆ (𝑎 × 𝑎)) |
102 | 101 | ssbrd 5096 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑠𝑣 → 𝑤(𝑎 × 𝑎)𝑣)) |
103 | 99, 102 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤(𝑎 × 𝑎)𝑣) |
104 | | brxp 5598 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑤(𝑎 × 𝑎)𝑣 ↔ (𝑤 ∈ 𝑎 ∧ 𝑣 ∈ 𝑎)) |
105 | 104 | simplbi 501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑤(𝑎 × 𝑎)𝑣 → 𝑤 ∈ 𝑎) |
106 | 103, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑎) |
107 | 73, 106 | elind 4108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ (𝑛 ∩ 𝑎)) |
108 | | breq1 5056 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 = 𝑤 → (𝑧𝑠𝑣 ↔ 𝑤𝑠𝑣)) |
109 | 108 | rspcev 3537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑤 ∈ (𝑛 ∩ 𝑎) ∧ 𝑤𝑠𝑣) → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣) |
110 | 107, 99, 109 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣) |
111 | 72 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑛) |
112 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑏 ⊆ 𝑎) |
113 | 90 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑏) |
114 | 112, 113 | sseldd 3902 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑎) |
115 | 111, 114 | elind 4108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ (𝑛 ∩ 𝑎)) |
116 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑡𝑣) |
117 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 = (𝑠 ∩ (𝑎 × 𝑏))) |
118 | | inss1 4143 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑠 ∩ (𝑎 × 𝑏)) ⊆ 𝑠 |
119 | 117, 118 | eqsstrdi 3955 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 ⊆ 𝑠) |
120 | 119 | ssbrd 5096 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑤𝑡𝑣 → 𝑤𝑠𝑣)) |
121 | 116, 120 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑠𝑣) |
122 | 115, 121,
109 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣) |
123 | 5 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝐴 ∈ 𝑉) |
124 | | fpwwe2.3 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) |
125 | 124 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) |
126 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑎𝑊𝑠) |
127 | 4, 123, 125, 126, 79 | fpwwe2lem9 10253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → ((𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏))))) |
128 | 75, 77, 78, 127 | syl12anc 837 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → ((𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏))))) |
129 | 110, 122,
128 | mpjaodan 959 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣) |
130 | 129 | expr 460 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ (𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡)) → (𝑤𝑡𝑣 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)) |
131 | 71, 130 | syl5bir 246 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ (𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡)) → (〈𝑤, 𝑣〉 ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)) |
132 | 131 | expr 460 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (𝑏𝑊𝑡 → (〈𝑤, 𝑣〉 ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣))) |
133 | 132 | exlimdv 1941 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (∃𝑏 𝑏𝑊𝑡 → (〈𝑤, 𝑣〉 ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣))) |
134 | 70, 133 | syl5bi 245 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (𝑡 ∈ ran 𝑊 → (〈𝑤, 𝑣〉 ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣))) |
135 | 134 | rexlimdv 3202 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (∃𝑡 ∈ ran 𝑊〈𝑤, 𝑣〉 ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)) |
136 | 68, 135 | syl5bi 245 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (𝑤∪ ran 𝑊 𝑣 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)) |
137 | 65, 136 | mtod 201 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → ¬ 𝑤∪ ran 𝑊 𝑣) |
138 | 137 | ralrimiva 3105 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) → ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣) |
139 | 60, 62, 138 | reximssdv 3195 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣) |
140 | 139 | exp32 424 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → (𝑎𝑊𝑠 → (𝑦 ∈ 𝑎 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))) |
141 | 140 | exlimdv 1941 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → (∃𝑠 𝑎𝑊𝑠 → (𝑦 ∈ 𝑎 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))) |
142 | 3, 141 | syl5bi 245 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → (𝑎 ∈ dom 𝑊 → (𝑦 ∈ 𝑎 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))) |
143 | 142 | rexlimdv 3202 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → (∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)) |
144 | 45, 143 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣) |
145 | 144 | expr 460 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ⊆ 𝑋) → (𝑦 ∈ 𝑛 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)) |
146 | 145 | exlimdv 1941 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ⊆ 𝑋) → (∃𝑦 𝑦 ∈ 𝑛 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)) |
147 | 39, 146 | syl5bi 245 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ⊆ 𝑋) → (𝑛 ≠ ∅ → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)) |
148 | 147 | expimpd 457 |
. . . . . . 7
⊢ (𝜑 → ((𝑛 ⊆ 𝑋 ∧ 𝑛 ≠ ∅) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)) |
149 | 148 | alrimiv 1935 |
. . . . . 6
⊢ (𝜑 → ∀𝑛((𝑛 ⊆ 𝑋 ∧ 𝑛 ≠ ∅) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)) |
150 | | df-fr 5509 |
. . . . . 6
⊢ (∪ ran 𝑊 Fr 𝑋 ↔ ∀𝑛((𝑛 ⊆ 𝑋 ∧ 𝑛 ≠ ∅) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)) |
151 | 149, 150 | sylibr 237 |
. . . . 5
⊢ (𝜑 → ∪ ran 𝑊 Fr 𝑋) |
152 | 1 | eleq2i 2829 |
. . . . . . . . . 10
⊢ (𝑤 ∈ 𝑋 ↔ 𝑤 ∈ ∪ dom
𝑊) |
153 | | eluni2 4823 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ∪ dom 𝑊 ↔ ∃𝑏 ∈ dom 𝑊 𝑤 ∈ 𝑏) |
154 | 152, 153 | bitri 278 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝑋 ↔ ∃𝑏 ∈ dom 𝑊 𝑤 ∈ 𝑏) |
155 | 44, 154 | anbi12i 630 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ↔ (∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎 ∧ ∃𝑏 ∈ dom 𝑊 𝑤 ∈ 𝑏)) |
156 | | reeanv 3279 |
. . . . . . . 8
⊢
(∃𝑎 ∈ dom
𝑊∃𝑏 ∈ dom 𝑊(𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) ↔ (∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎 ∧ ∃𝑏 ∈ dom 𝑊 𝑤 ∈ 𝑏)) |
157 | 155, 156 | bitr4i 281 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ↔ ∃𝑎 ∈ dom 𝑊∃𝑏 ∈ dom 𝑊(𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) |
158 | | vex 3412 |
. . . . . . . . . . . 12
⊢ 𝑏 ∈ V |
159 | 158 | eldm 5769 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ dom 𝑊 ↔ ∃𝑡 𝑏𝑊𝑡) |
160 | 3, 159 | anbi12i 630 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ dom 𝑊 ∧ 𝑏 ∈ dom 𝑊) ↔ (∃𝑠 𝑎𝑊𝑠 ∧ ∃𝑡 𝑏𝑊𝑡)) |
161 | | exdistrv 1964 |
. . . . . . . . . 10
⊢
(∃𝑠∃𝑡(𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡) ↔ (∃𝑠 𝑎𝑊𝑠 ∧ ∃𝑡 𝑏𝑊𝑡)) |
162 | 160, 161 | bitr4i 281 |
. . . . . . . . 9
⊢ ((𝑎 ∈ dom 𝑊 ∧ 𝑏 ∈ dom 𝑊) ↔ ∃𝑠∃𝑡(𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) |
163 | 82 | simprd 499 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → (𝑡 We 𝑏 ∧ ∀𝑦 ∈ 𝑏 [(◡𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦)) |
164 | 163 | simpld 498 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑡 We 𝑏) |
165 | 164 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 We 𝑏) |
166 | | weso 5542 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 We 𝑏 → 𝑡 Or 𝑏) |
167 | 165, 166 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 Or 𝑏) |
168 | | simprl 771 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑎 ⊆ 𝑏) |
169 | | simplrl 777 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑦 ∈ 𝑎) |
170 | 168, 169 | sseldd 3902 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑦 ∈ 𝑏) |
171 | | simplrr 778 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑏) |
172 | | solin 5493 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 Or 𝑏 ∧ (𝑦 ∈ 𝑏 ∧ 𝑤 ∈ 𝑏)) → (𝑦𝑡𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑡𝑦)) |
173 | 167, 170,
171, 172 | syl12anc 837 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦𝑡𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑡𝑦)) |
174 | 21 | relelrni 5818 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏𝑊𝑡 → 𝑡 ∈ ran 𝑊) |
175 | 174 | ad2antll 729 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑡 ∈ ran 𝑊) |
176 | 175 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ∈ ran 𝑊) |
177 | | elssuni 4851 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ ran 𝑊 → 𝑡 ⊆ ∪ ran
𝑊) |
178 | 176, 177 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ⊆ ∪ ran
𝑊) |
179 | 178 | ssbrd 5096 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦𝑡𝑤 → 𝑦∪ ran 𝑊 𝑤)) |
180 | | idd 24 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦 = 𝑤 → 𝑦 = 𝑤)) |
181 | 178 | ssbrd 5096 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑡𝑦 → 𝑤∪ ran 𝑊 𝑦)) |
182 | 179, 180,
181 | 3orim123d 1446 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → ((𝑦𝑡𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑡𝑦) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))) |
183 | 173, 182 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)) |
184 | 49 | adantrr 717 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑠 We 𝑎) |
185 | 184 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 We 𝑎) |
186 | | weso 5542 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 We 𝑎 → 𝑠 Or 𝑎) |
187 | 185, 186 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 Or 𝑎) |
188 | | simplrl 777 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑦 ∈ 𝑎) |
189 | | simprl 771 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑏 ⊆ 𝑎) |
190 | | simplrr 778 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑏) |
191 | 189, 190 | sseldd 3902 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑎) |
192 | | solin 5493 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 Or 𝑎 ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → (𝑦𝑠𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑠𝑦)) |
193 | 187, 188,
191, 192 | syl12anc 837 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦𝑠𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑠𝑦)) |
194 | 21 | relelrni 5818 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎𝑊𝑠 → 𝑠 ∈ ran 𝑊) |
195 | 194 | ad2antrl 728 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑠 ∈ ran 𝑊) |
196 | 195 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 ∈ ran 𝑊) |
197 | | elssuni 4851 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ran 𝑊 → 𝑠 ⊆ ∪ ran
𝑊) |
198 | 196, 197 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 ⊆ ∪ ran
𝑊) |
199 | 198 | ssbrd 5096 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦𝑠𝑤 → 𝑦∪ ran 𝑊 𝑤)) |
200 | | idd 24 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦 = 𝑤 → 𝑦 = 𝑤)) |
201 | 198 | ssbrd 5096 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑤𝑠𝑦 → 𝑤∪ ran 𝑊 𝑦)) |
202 | 199, 200,
201 | 3orim123d 1446 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → ((𝑦𝑠𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑠𝑦) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))) |
203 | 193, 202 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)) |
204 | 127 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) → ((𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏))))) |
205 | 183, 203,
204 | mpjaodan 959 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)) |
206 | 205 | exp31 423 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡) → ((𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)))) |
207 | 206 | exlimdvv 1942 |
. . . . . . . . 9
⊢ (𝜑 → (∃𝑠∃𝑡(𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡) → ((𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)))) |
208 | 162, 207 | syl5bi 245 |
. . . . . . . 8
⊢ (𝜑 → ((𝑎 ∈ dom 𝑊 ∧ 𝑏 ∈ dom 𝑊) → ((𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)))) |
209 | 208 | rexlimdvv 3212 |
. . . . . . 7
⊢ (𝜑 → (∃𝑎 ∈ dom 𝑊∃𝑏 ∈ dom 𝑊(𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))) |
210 | 157, 209 | syl5bi 245 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))) |
211 | 210 | ralrimivv 3111 |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)) |
212 | | dfwe2 7559 |
. . . . 5
⊢ (∪ ran 𝑊 We 𝑋 ↔ (∪ ran
𝑊 Fr 𝑋 ∧ ∀𝑦 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))) |
213 | 151, 211,
212 | sylanbrc 586 |
. . . 4
⊢ (𝜑 → ∪ ran 𝑊 We 𝑋) |
214 | 4 | fpwwe2cbv 10244 |
. . . . . . . . . . . . 13
⊢ 𝑊 = {〈𝑧, 𝑡〉 ∣ ((𝑧 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑧 × 𝑧)) ∧ (𝑡 We 𝑧 ∧ ∀𝑤 ∈ 𝑧 [(◡𝑡 “ {𝑤}) / 𝑏](𝑏𝐹(𝑡 ∩ (𝑏 × 𝑏))) = 𝑤))} |
215 | 5 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝐴 ∈ 𝑉) |
216 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎𝑊𝑠) |
217 | 214, 215,
216 | fpwwe2lem3 10247 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎𝑊𝑠) ∧ 𝑦 ∈ 𝑎) → ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) = 𝑦) |
218 | 217 | anasss 470 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) = 𝑦) |
219 | | cnvimass 5949 |
. . . . . . . . . . . . 13
⊢ (◡∪ ran 𝑊 “ {𝑦}) ⊆ dom ∪
ran 𝑊 |
220 | 5, 17 | ssexd 5217 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑋 ∈ V) |
221 | 220, 220 | xpexd 7536 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑋 × 𝑋) ∈ V) |
222 | 221, 37 | ssexd 5217 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∪ ran 𝑊 ∈ V) |
223 | 222 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ∪ ran
𝑊 ∈
V) |
224 | 223 | dmexd 7683 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → dom ∪
ran 𝑊 ∈
V) |
225 | | ssexg 5216 |
. . . . . . . . . . . . 13
⊢ (((◡∪ ran 𝑊 “ {𝑦}) ⊆ dom ∪
ran 𝑊 ∧ dom ∪ ran 𝑊 ∈ V) → (◡∪ ran 𝑊 “ {𝑦}) ∈ V) |
226 | 219, 224,
225 | sylancr 590 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (◡∪ ran 𝑊 “ {𝑦}) ∈ V) |
227 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = (◡∪ ran 𝑊 “ {𝑦}) → 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) |
228 | | olc 868 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = 𝑦 → (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) |
229 | | df-br 5054 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧∪ ran
𝑊 𝑤 ↔ 〈𝑧, 𝑤〉 ∈ ∪
ran 𝑊) |
230 | | eluni2 4823 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(〈𝑧, 𝑤〉 ∈ ∪ ran 𝑊 ↔ ∃𝑡 ∈ ran 𝑊〈𝑧, 𝑤〉 ∈ 𝑡) |
231 | 229, 230 | bitri 278 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧∪ ran
𝑊 𝑤 ↔ ∃𝑡 ∈ ran 𝑊〈𝑧, 𝑤〉 ∈ 𝑡) |
232 | | df-br 5054 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑧𝑡𝑤 ↔ 〈𝑧, 𝑤〉 ∈ 𝑡) |
233 | 84 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ⊆ (𝑏 × 𝑏)) |
234 | 233 | ssbrd 5096 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → 𝑧(𝑏 × 𝑏)𝑤)) |
235 | | brxp 5598 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑧(𝑏 × 𝑏)𝑤 ↔ (𝑧 ∈ 𝑏 ∧ 𝑤 ∈ 𝑏)) |
236 | 235 | simplbi 501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑧(𝑏 × 𝑏)𝑤 → 𝑧 ∈ 𝑏) |
237 | 234, 236 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → 𝑧 ∈ 𝑏)) |
238 | 20 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑠 ⊆ (𝑎 × 𝑎)) |
239 | 238 | ssbrd 5096 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → (𝑤𝑠𝑦 → 𝑤(𝑎 × 𝑎)𝑦)) |
240 | 239 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → 𝑤(𝑎 × 𝑎)𝑦) |
241 | | brxp 5598 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑤(𝑎 × 𝑎)𝑦 ↔ (𝑤 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎)) |
242 | 241 | simplbi 501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑤(𝑎 × 𝑎)𝑦 → 𝑤 ∈ 𝑎) |
243 | 240, 242 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → 𝑤 ∈ 𝑎) |
244 | 243 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → (𝑦 ∈ 𝑎 → 𝑤 ∈ 𝑎)) |
245 | | elequ1 2117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝑎 ↔ 𝑦 ∈ 𝑎)) |
246 | 245 | biimprd 251 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑤 = 𝑦 → (𝑦 ∈ 𝑎 → 𝑤 ∈ 𝑎)) |
247 | 246 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ 𝑤 = 𝑦) → (𝑦 ∈ 𝑎 → 𝑤 ∈ 𝑎)) |
248 | 244, 247 | jaodan 958 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (𝑦 ∈ 𝑎 → 𝑤 ∈ 𝑎)) |
249 | 248 | impr 458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) → 𝑤 ∈ 𝑎) |
250 | 249 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑎) |
251 | 237, 250 | jctird 530 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → (𝑧 ∈ 𝑏 ∧ 𝑤 ∈ 𝑎))) |
252 | | brxp 5598 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑧(𝑏 × 𝑎)𝑤 ↔ (𝑧 ∈ 𝑏 ∧ 𝑤 ∈ 𝑎)) |
253 | 251, 252 | syl6ibr 255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → 𝑧(𝑏 × 𝑎)𝑤)) |
254 | 253 | ancld 554 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → (𝑧𝑡𝑤 ∧ 𝑧(𝑏 × 𝑎)𝑤))) |
255 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) |
256 | 255 | breqd 5064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑠𝑤 ↔ 𝑧(𝑡 ∩ (𝑏 × 𝑎))𝑤)) |
257 | | brin 5105 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑧(𝑡 ∩ (𝑏 × 𝑎))𝑤 ↔ (𝑧𝑡𝑤 ∧ 𝑧(𝑏 × 𝑎)𝑤)) |
258 | 256, 257 | bitrdi 290 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑠𝑤 ↔ (𝑧𝑡𝑤 ∧ 𝑧(𝑏 × 𝑎)𝑤))) |
259 | 254, 258 | sylibrd 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → 𝑧𝑠𝑤)) |
260 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 = (𝑠 ∩ (𝑎 × 𝑏))) |
261 | 260, 118 | eqsstrdi 3955 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 ⊆ 𝑠) |
262 | 261 | ssbrd 5096 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑧𝑡𝑤 → 𝑧𝑠𝑤)) |
263 | 127 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) → ((𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏))))) |
264 | 259, 262,
263 | mpjaodan 959 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) → (𝑧𝑡𝑤 → 𝑧𝑠𝑤)) |
265 | 232, 264 | syl5bir 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) → (〈𝑧, 𝑤〉 ∈ 𝑡 → 𝑧𝑠𝑤)) |
266 | 265 | exp32 424 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) → (𝑦 ∈ 𝑎 → (〈𝑧, 𝑤〉 ∈ 𝑡 → 𝑧𝑠𝑤)))) |
267 | 266 | expr 460 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑏𝑊𝑡 → ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) → (𝑦 ∈ 𝑎 → (〈𝑧, 𝑤〉 ∈ 𝑡 → 𝑧𝑠𝑤))))) |
268 | 267 | com24 95 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑦 ∈ 𝑎 → ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) → (𝑏𝑊𝑡 → (〈𝑧, 𝑤〉 ∈ 𝑡 → 𝑧𝑠𝑤))))) |
269 | 268 | impr 458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) → (𝑏𝑊𝑡 → (〈𝑧, 𝑤〉 ∈ 𝑡 → 𝑧𝑠𝑤)))) |
270 | 269 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (𝑏𝑊𝑡 → (〈𝑧, 𝑤〉 ∈ 𝑡 → 𝑧𝑠𝑤))) |
271 | 270 | exlimdv 1941 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (∃𝑏 𝑏𝑊𝑡 → (〈𝑧, 𝑤〉 ∈ 𝑡 → 𝑧𝑠𝑤))) |
272 | 70, 271 | syl5bi 245 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (𝑡 ∈ ran 𝑊 → (〈𝑧, 𝑤〉 ∈ 𝑡 → 𝑧𝑠𝑤))) |
273 | 272 | rexlimdv 3202 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (∃𝑡 ∈ ran 𝑊〈𝑧, 𝑤〉 ∈ 𝑡 → 𝑧𝑠𝑤)) |
274 | 231, 273 | syl5bi 245 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤)) |
275 | 228, 274 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑤 = 𝑦) → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤)) |
276 | 275 | ex 416 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑤 = 𝑦 → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤))) |
277 | 276 | alrimiv 1935 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ∀𝑤(𝑤 = 𝑦 → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤))) |
278 | | breq2 5057 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑦 → (𝑧∪ ran 𝑊 𝑤 ↔ 𝑧∪ ran 𝑊 𝑦)) |
279 | | breq2 5057 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑦 → (𝑧𝑠𝑤 ↔ 𝑧𝑠𝑦)) |
280 | 278, 279 | imbi12d 348 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑦 → ((𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤) ↔ (𝑧∪ ran 𝑊 𝑦 → 𝑧𝑠𝑦))) |
281 | 280 | equsalvw 2012 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑤(𝑤 = 𝑦 → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤)) ↔ (𝑧∪ ran 𝑊 𝑦 → 𝑧𝑠𝑦)) |
282 | 277, 281 | sylib 221 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑧∪ ran 𝑊 𝑦 → 𝑧𝑠𝑦)) |
283 | 194 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑠 ∈ ran 𝑊) |
284 | 283, 197 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑠 ⊆ ∪ ran
𝑊) |
285 | 284 | ssbrd 5096 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑧𝑠𝑦 → 𝑧∪ ran 𝑊 𝑦)) |
286 | 282, 285 | impbid 215 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑧∪ ran 𝑊 𝑦 ↔ 𝑧𝑠𝑦)) |
287 | | vex 3412 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑧 ∈ V |
288 | 287 | eliniseg 5962 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ V → (𝑧 ∈ (◡∪ ran 𝑊 “ {𝑦}) ↔ 𝑧∪ ran 𝑊 𝑦)) |
289 | 288 | elv 3414 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ (◡∪ ran 𝑊 “ {𝑦}) ↔ 𝑧∪ ran 𝑊 𝑦) |
290 | 287 | eliniseg 5962 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ V → (𝑧 ∈ (◡𝑠 “ {𝑦}) ↔ 𝑧𝑠𝑦)) |
291 | 290 | elv 3414 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ (◡𝑠 “ {𝑦}) ↔ 𝑧𝑠𝑦) |
292 | 286, 289,
291 | 3bitr4g 317 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑧 ∈ (◡∪ ran 𝑊 “ {𝑦}) ↔ 𝑧 ∈ (◡𝑠 “ {𝑦}))) |
293 | 292 | eqrdv 2735 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (◡∪ ran 𝑊 “ {𝑦}) = (◡𝑠 “ {𝑦})) |
294 | 227, 293 | sylan9eqr 2800 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → 𝑢 = (◡𝑠 “ {𝑦})) |
295 | 294 | sqxpeqd 5583 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (𝑢 × 𝑢) = ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) |
296 | 295 | ineq2d 4127 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (∪ ran
𝑊 ∩ (𝑢 × 𝑢)) = (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) |
297 | | relinxp 5684 |
. . . . . . . . . . . . . . . . 17
⊢ Rel
(∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) |
298 | | relinxp 5684 |
. . . . . . . . . . . . . . . . 17
⊢ Rel
(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) |
299 | | vex 3412 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑤 ∈ V |
300 | 299 | eliniseg 5962 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ V → (𝑤 ∈ (◡𝑠 “ {𝑦}) ↔ 𝑤𝑠𝑦)) |
301 | 290, 300 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ V → ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ↔ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦))) |
302 | 301 | elv 3414 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ↔ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)) |
303 | | orc 867 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤𝑠𝑦 → (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) |
304 | 303, 274 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑤𝑠𝑦) → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤)) |
305 | 304 | adantrl 716 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)) → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤)) |
306 | 284 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)) → 𝑠 ⊆ ∪ ran
𝑊) |
307 | 306 | ssbrd 5096 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)) → (𝑧𝑠𝑤 → 𝑧∪ ran 𝑊 𝑤)) |
308 | 305, 307 | impbid 215 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)) → (𝑧∪ ran 𝑊 𝑤 ↔ 𝑧𝑠𝑤)) |
309 | 302, 308 | sylan2b 597 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦}))) → (𝑧∪ ran 𝑊 𝑤 ↔ 𝑧𝑠𝑤)) |
310 | 309 | pm5.32da 582 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧∪ ran 𝑊 𝑤) ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤))) |
311 | | df-br 5054 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧(∪
ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))𝑤 ↔ 〈𝑧, 𝑤〉 ∈ (∪
ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) |
312 | | brinxp2 5626 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧(∪
ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))𝑤 ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧∪ ran 𝑊 𝑤)) |
313 | 311, 312 | bitr3i 280 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑧, 𝑤〉 ∈ (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧∪ ran 𝑊 𝑤)) |
314 | | df-br 5054 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))𝑤 ↔ 〈𝑧, 𝑤〉 ∈ (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) |
315 | | brinxp2 5626 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))𝑤 ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤)) |
316 | 314, 315 | bitr3i 280 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑧, 𝑤〉 ∈ (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤)) |
317 | 310, 313,
316 | 3bitr4g 317 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (〈𝑧, 𝑤〉 ∈ (∪
ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) ↔ 〈𝑧, 𝑤〉 ∈ (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))) |
318 | 297, 298,
317 | eqrelrdv 5662 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (∪ ran
𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) = (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) |
319 | 318 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (∪ ran
𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) = (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) |
320 | 296, 319 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (∪ ran
𝑊 ∩ (𝑢 × 𝑢)) = (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) |
321 | 294, 320 | oveq12d 7231 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))) |
322 | 321 | eqeq1d 2739 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → ((𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) = 𝑦)) |
323 | 226, 322 | sbcied 3739 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ([(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) = 𝑦)) |
324 | 218, 323 | mpbird 260 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦) |
325 | 324 | exp32 424 |
. . . . . . . . 9
⊢ (𝜑 → (𝑎𝑊𝑠 → (𝑦 ∈ 𝑎 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))) |
326 | 325 | exlimdv 1941 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑠 𝑎𝑊𝑠 → (𝑦 ∈ 𝑎 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))) |
327 | 3, 326 | syl5bi 245 |
. . . . . . 7
⊢ (𝜑 → (𝑎 ∈ dom 𝑊 → (𝑦 ∈ 𝑎 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))) |
328 | 327 | rexlimdv 3202 |
. . . . . 6
⊢ (𝜑 → (∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)) |
329 | 44, 328 | syl5bi 245 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝑋 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)) |
330 | 329 | ralrimiv 3104 |
. . . 4
⊢ (𝜑 → ∀𝑦 ∈ 𝑋 [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦) |
331 | 213, 330 | jca 515 |
. . 3
⊢ (𝜑 → (∪ ran 𝑊 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)) |
332 | 4, 5 | fpwwe2lem2 10246 |
. . 3
⊢ (𝜑 → (𝑋𝑊∪ ran 𝑊 ↔ ((𝑋 ⊆ 𝐴 ∧ ∪ ran
𝑊 ⊆ (𝑋 × 𝑋)) ∧ (∪ ran
𝑊 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))) |
333 | 38, 331, 332 | mpbir2and 713 |
. 2
⊢ (𝜑 → 𝑋𝑊∪ ran 𝑊) |
334 | 21 | releldmi 5817 |
. 2
⊢ (𝑋𝑊∪ ran 𝑊 → 𝑋 ∈ dom 𝑊) |
335 | 333, 334 | syl 17 |
1
⊢ (𝜑 → 𝑋 ∈ dom 𝑊) |