Step | Hyp | Ref
| Expression |
1 | | simpl2 1192 |
. . . . . . 7
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → 𝑅 Se 𝐴) |
2 | | weiun.1 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑤 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢)) |
3 | | weiun.2 |
. . . . . . . . . 10
⊢ 𝑇 = {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))} |
4 | | simpl1 1191 |
. . . . . . . . . 10
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → 𝑅 We 𝐴) |
5 | 2, 3, 4, 1 | weiunlem2 36431 |
. . . . . . . . 9
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑡 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ∧ ∀𝑠 ∈ 𝐴 ∀𝑡 ∈ ⦋ 𝑠 / 𝑥⦌𝐵 ¬ 𝑠𝑅(𝐹‘𝑡))) |
6 | 5 | simp1d 1142 |
. . . . . . . 8
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → 𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴) |
7 | | simpr 484 |
. . . . . . . 8
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
8 | 6, 7 | ffvelcdmd 7121 |
. . . . . . 7
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → (𝐹‘𝑝) ∈ 𝐴) |
9 | | seex 5659 |
. . . . . . 7
⊢ ((𝑅 Se 𝐴 ∧ (𝐹‘𝑝) ∈ 𝐴) → {𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∈ V) |
10 | 1, 8, 9 | syl2anc 583 |
. . . . . 6
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → {𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∈ V) |
11 | | snex 5451 |
. . . . . 6
⊢ {(𝐹‘𝑝)} ∈ V |
12 | | unexg 7780 |
. . . . . 6
⊢ (({𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∈ V ∧ {(𝐹‘𝑝)} ∈ V) → ({𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∪ {(𝐹‘𝑝)}) ∈ V) |
13 | 10, 11, 12 | sylancl 585 |
. . . . 5
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → ({𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∪ {(𝐹‘𝑝)}) ∈ V) |
14 | | ssrab2 4103 |
. . . . . . . 8
⊢ {𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ⊆ 𝐴 |
15 | 14 | a1i 11 |
. . . . . . 7
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → {𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ⊆ 𝐴) |
16 | 8 | snssd 4834 |
. . . . . . 7
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → {(𝐹‘𝑝)} ⊆ 𝐴) |
17 | 15, 16 | unssd 4215 |
. . . . . 6
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → ({𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∪ {(𝐹‘𝑝)}) ⊆ 𝐴) |
18 | | simpl3 1193 |
. . . . . . . 8
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) |
19 | | elex 3509 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V) |
20 | 19 | ralimi 3089 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V) |
21 | 18, 20 | syl 17 |
. . . . . . 7
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → ∀𝑥 ∈ 𝐴 𝐵 ∈ V) |
22 | | nfv 1913 |
. . . . . . . 8
⊢
Ⅎ𝑠 𝐵 ∈ V |
23 | | nfcsb1v 3946 |
. . . . . . . . 9
⊢
Ⅎ𝑥⦋𝑠 / 𝑥⦌𝐵 |
24 | 23 | nfel1 2925 |
. . . . . . . 8
⊢
Ⅎ𝑥⦋𝑠 / 𝑥⦌𝐵 ∈ V |
25 | | csbeq1a 3935 |
. . . . . . . . 9
⊢ (𝑥 = 𝑠 → 𝐵 = ⦋𝑠 / 𝑥⦌𝐵) |
26 | 25 | eleq1d 2829 |
. . . . . . . 8
⊢ (𝑥 = 𝑠 → (𝐵 ∈ V ↔ ⦋𝑠 / 𝑥⦌𝐵 ∈ V)) |
27 | 22, 24, 26 | cbvralw 3312 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ V ↔ ∀𝑠 ∈ 𝐴 ⦋𝑠 / 𝑥⦌𝐵 ∈ V) |
28 | 21, 27 | sylib 218 |
. . . . . 6
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → ∀𝑠 ∈ 𝐴 ⦋𝑠 / 𝑥⦌𝐵 ∈ V) |
29 | | ssralv 4077 |
. . . . . 6
⊢ (({𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∪ {(𝐹‘𝑝)}) ⊆ 𝐴 → (∀𝑠 ∈ 𝐴 ⦋𝑠 / 𝑥⦌𝐵 ∈ V → ∀𝑠 ∈ ({𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∪ {(𝐹‘𝑝)})⦋𝑠 / 𝑥⦌𝐵 ∈ V)) |
30 | 17, 28, 29 | sylc 65 |
. . . . 5
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → ∀𝑠 ∈ ({𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∪ {(𝐹‘𝑝)})⦋𝑠 / 𝑥⦌𝐵 ∈ V) |
31 | | iunexg 8006 |
. . . . 5
⊢ ((({𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∪ {(𝐹‘𝑝)}) ∈ V ∧ ∀𝑠 ∈ ({𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∪ {(𝐹‘𝑝)})⦋𝑠 / 𝑥⦌𝐵 ∈ V) → ∪ 𝑠 ∈ ({𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∪ {(𝐹‘𝑝)})⦋𝑠 / 𝑥⦌𝐵 ∈ V) |
32 | 13, 30, 31 | syl2anc 583 |
. . . 4
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → ∪
𝑠 ∈ ({𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∪ {(𝐹‘𝑝)})⦋𝑠 / 𝑥⦌𝐵 ∈ V) |
33 | 6 | 3ad2ant1 1133 |
. . . . . . . . 9
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ 𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑞𝑇𝑝) → 𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴) |
34 | | simp2 1137 |
. . . . . . . . 9
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ 𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑞𝑇𝑝) → 𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
35 | 33, 34 | ffvelcdmd 7121 |
. . . . . . . 8
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ 𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑞𝑇𝑝) → (𝐹‘𝑞) ∈ 𝐴) |
36 | | breq1 5169 |
. . . . . . . . . 10
⊢ (𝑟 = (𝐹‘𝑞) → (𝑟𝑅(𝐹‘𝑝) ↔ (𝐹‘𝑞)𝑅(𝐹‘𝑝))) |
37 | 36 | elrab 3708 |
. . . . . . . . 9
⊢ ((𝐹‘𝑞) ∈ {𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ↔ ((𝐹‘𝑞) ∈ 𝐴 ∧ (𝐹‘𝑞)𝑅(𝐹‘𝑝))) |
38 | | elun1 4205 |
. . . . . . . . 9
⊢ ((𝐹‘𝑞) ∈ {𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} → (𝐹‘𝑞) ∈ ({𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∪ {(𝐹‘𝑝)})) |
39 | 37, 38 | sylbir 235 |
. . . . . . . 8
⊢ (((𝐹‘𝑞) ∈ 𝐴 ∧ (𝐹‘𝑞)𝑅(𝐹‘𝑝)) → (𝐹‘𝑞) ∈ ({𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∪ {(𝐹‘𝑝)})) |
40 | 35, 39 | sylan 579 |
. . . . . . 7
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ 𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑞𝑇𝑝) ∧ (𝐹‘𝑞)𝑅(𝐹‘𝑝)) → (𝐹‘𝑞) ∈ ({𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∪ {(𝐹‘𝑝)})) |
41 | | fvex 6935 |
. . . . . . . . . 10
⊢ (𝐹‘𝑞) ∈ V |
42 | 41 | elsn 4663 |
. . . . . . . . 9
⊢ ((𝐹‘𝑞) ∈ {(𝐹‘𝑝)} ↔ (𝐹‘𝑞) = (𝐹‘𝑝)) |
43 | | elun2 4206 |
. . . . . . . . 9
⊢ ((𝐹‘𝑞) ∈ {(𝐹‘𝑝)} → (𝐹‘𝑞) ∈ ({𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∪ {(𝐹‘𝑝)})) |
44 | 42, 43 | sylbir 235 |
. . . . . . . 8
⊢ ((𝐹‘𝑞) = (𝐹‘𝑝) → (𝐹‘𝑞) ∈ ({𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∪ {(𝐹‘𝑝)})) |
45 | 44 | ad2antrl 727 |
. . . . . . 7
⊢
(((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ 𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑞𝑇𝑝) ∧ ((𝐹‘𝑞) = (𝐹‘𝑝) ∧ 𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑝)) → (𝐹‘𝑞) ∈ ({𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∪ {(𝐹‘𝑝)})) |
46 | 2, 3 | weiunlem1 36430 |
. . . . . . . . 9
⊢ (𝑞𝑇𝑝 ↔ ((𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑞)𝑅(𝐹‘𝑝) ∨ ((𝐹‘𝑞) = (𝐹‘𝑝) ∧ 𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑝)))) |
47 | 46 | simprbi 496 |
. . . . . . . 8
⊢ (𝑞𝑇𝑝 → ((𝐹‘𝑞)𝑅(𝐹‘𝑝) ∨ ((𝐹‘𝑞) = (𝐹‘𝑝) ∧ 𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑝))) |
48 | 47 | 3ad2ant3 1135 |
. . . . . . 7
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ 𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑞𝑇𝑝) → ((𝐹‘𝑞)𝑅(𝐹‘𝑝) ∨ ((𝐹‘𝑞) = (𝐹‘𝑝) ∧ 𝑞⦋(𝐹‘𝑞) / 𝑥⦌𝑆𝑝))) |
49 | 40, 45, 48 | mpjaodan 959 |
. . . . . 6
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ 𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑞𝑇𝑝) → (𝐹‘𝑞) ∈ ({𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∪ {(𝐹‘𝑝)})) |
50 | | id 22 |
. . . . . . . 8
⊢ (𝑡 = 𝑞 → 𝑡 = 𝑞) |
51 | | fveq2 6922 |
. . . . . . . . 9
⊢ (𝑡 = 𝑞 → (𝐹‘𝑡) = (𝐹‘𝑞)) |
52 | 51 | csbeq1d 3925 |
. . . . . . . 8
⊢ (𝑡 = 𝑞 → ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 = ⦋(𝐹‘𝑞) / 𝑥⦌𝐵) |
53 | 50, 52 | eleq12d 2838 |
. . . . . . 7
⊢ (𝑡 = 𝑞 → (𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ↔ 𝑞 ∈ ⦋(𝐹‘𝑞) / 𝑥⦌𝐵)) |
54 | 5 | simp2d 1143 |
. . . . . . . 8
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → ∀𝑡 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵) |
55 | 54 | 3ad2ant1 1133 |
. . . . . . 7
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ 𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑞𝑇𝑝) → ∀𝑡 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵) |
56 | 53, 55, 34 | rspcdva 3636 |
. . . . . 6
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ 𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑞𝑇𝑝) → 𝑞 ∈ ⦋(𝐹‘𝑞) / 𝑥⦌𝐵) |
57 | | csbeq1 3924 |
. . . . . . 7
⊢ (𝑠 = (𝐹‘𝑞) → ⦋𝑠 / 𝑥⦌𝐵 = ⦋(𝐹‘𝑞) / 𝑥⦌𝐵) |
58 | 57 | eliuni 5021 |
. . . . . 6
⊢ (((𝐹‘𝑞) ∈ ({𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∪ {(𝐹‘𝑝)}) ∧ 𝑞 ∈ ⦋(𝐹‘𝑞) / 𝑥⦌𝐵) → 𝑞 ∈ ∪
𝑠 ∈ ({𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∪ {(𝐹‘𝑝)})⦋𝑠 / 𝑥⦌𝐵) |
59 | 49, 56, 58 | syl2anc 583 |
. . . . 5
⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ 𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑞𝑇𝑝) → 𝑞 ∈ ∪
𝑠 ∈ ({𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∪ {(𝐹‘𝑝)})⦋𝑠 / 𝑥⦌𝐵) |
60 | 59 | rabssdv 4098 |
. . . 4
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → {𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∣ 𝑞𝑇𝑝} ⊆ ∪
𝑠 ∈ ({𝑟 ∈ 𝐴 ∣ 𝑟𝑅(𝐹‘𝑝)} ∪ {(𝐹‘𝑝)})⦋𝑠 / 𝑥⦌𝐵) |
61 | 32, 60 | ssexd 5342 |
. . 3
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) ∧ 𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → {𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∣ 𝑞𝑇𝑝} ∈ V) |
62 | 61 | ralrimiva 3152 |
. 2
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) → ∀𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵{𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∣ 𝑞𝑇𝑝} ∈ V) |
63 | | df-se 5653 |
. 2
⊢ (𝑇 Se ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑝 ∈ ∪
𝑥 ∈ 𝐴 𝐵{𝑞 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∣ 𝑞𝑇𝑝} ∈ V) |
64 | 62, 63 | sylibr 234 |
1
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) → 𝑇 Se ∪
𝑥 ∈ 𝐴 𝐵) |