| Step |
Hyp |
Ref |
Expression |
| 1 |
|
weiun.1 |
⊢ 𝐹 = ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) ) |
| 2 |
|
weiun.2 |
⊢ 𝑇 = { 〈 𝑦 , 𝑧 〉 ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) } |
| 3 |
|
simpl2 |
⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → 𝑅 Se 𝐴 ) |
| 4 |
|
simpl1 |
⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → 𝑅 We 𝐴 ) |
| 5 |
1 2 4 3
|
weiunlem2 |
⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 ∧ ∀ 𝑠 ∈ 𝐴 ∀ 𝑡 ∈ ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ¬ 𝑠 𝑅 ( 𝐹 ‘ 𝑡 ) ) ) |
| 6 |
5
|
simp1d |
⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 ) |
| 7 |
|
simpr |
⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) |
| 8 |
6 7
|
ffvelcdmd |
⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( 𝐹 ‘ 𝑝 ) ∈ 𝐴 ) |
| 9 |
|
seex |
⊢ ( ( 𝑅 Se 𝐴 ∧ ( 𝐹 ‘ 𝑝 ) ∈ 𝐴 ) → { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∈ V ) |
| 10 |
3 8 9
|
syl2anc |
⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∈ V ) |
| 11 |
|
snex |
⊢ { ( 𝐹 ‘ 𝑝 ) } ∈ V |
| 12 |
|
unexg |
⊢ ( ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∈ V ∧ { ( 𝐹 ‘ 𝑝 ) } ∈ V ) → ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ∈ V ) |
| 13 |
10 11 12
|
sylancl |
⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ∈ V ) |
| 14 |
|
ssrab2 |
⊢ { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ⊆ 𝐴 |
| 15 |
14
|
a1i |
⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ⊆ 𝐴 ) |
| 16 |
8
|
snssd |
⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → { ( 𝐹 ‘ 𝑝 ) } ⊆ 𝐴 ) |
| 17 |
15 16
|
unssd |
⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ⊆ 𝐴 ) |
| 18 |
|
simpl3 |
⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) |
| 19 |
|
elex |
⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ V ) |
| 20 |
19
|
ralimi |
⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ) |
| 21 |
18 20
|
syl |
⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ) |
| 22 |
|
nfv |
⊢ Ⅎ 𝑠 𝐵 ∈ V |
| 23 |
|
nfcsb1v |
⊢ Ⅎ 𝑥 ⦋ 𝑠 / 𝑥 ⦌ 𝐵 |
| 24 |
23
|
nfel1 |
⊢ Ⅎ 𝑥 ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ∈ V |
| 25 |
|
csbeq1a |
⊢ ( 𝑥 = 𝑠 → 𝐵 = ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ) |
| 26 |
25
|
eleq1d |
⊢ ( 𝑥 = 𝑠 → ( 𝐵 ∈ V ↔ ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ∈ V ) ) |
| 27 |
22 24 26
|
cbvralw |
⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ↔ ∀ 𝑠 ∈ 𝐴 ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ∈ V ) |
| 28 |
21 27
|
sylib |
⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ∀ 𝑠 ∈ 𝐴 ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ∈ V ) |
| 29 |
|
ssralv |
⊢ ( ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ⊆ 𝐴 → ( ∀ 𝑠 ∈ 𝐴 ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ∈ V → ∀ 𝑠 ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ∈ V ) ) |
| 30 |
17 28 29
|
sylc |
⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ∀ 𝑠 ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ∈ V ) |
| 31 |
|
iunexg |
⊢ ( ( ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ∈ V ∧ ∀ 𝑠 ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ∈ V ) → ∪ 𝑠 ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ∈ V ) |
| 32 |
13 30 31
|
syl2anc |
⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ∪ 𝑠 ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ∈ V ) |
| 33 |
6
|
3ad2ant1 |
⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 𝑇 𝑝 ) → 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 ) |
| 34 |
|
simp2 |
⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 𝑇 𝑝 ) → 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) |
| 35 |
33 34
|
ffvelcdmd |
⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 𝑇 𝑝 ) → ( 𝐹 ‘ 𝑞 ) ∈ 𝐴 ) |
| 36 |
|
breq1 |
⊢ ( 𝑟 = ( 𝐹 ‘ 𝑞 ) → ( 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) ↔ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ) ) |
| 37 |
36
|
elrab |
⊢ ( ( 𝐹 ‘ 𝑞 ) ∈ { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ↔ ( ( 𝐹 ‘ 𝑞 ) ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ) ) |
| 38 |
|
elun1 |
⊢ ( ( 𝐹 ‘ 𝑞 ) ∈ { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } → ( 𝐹 ‘ 𝑞 ) ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ) |
| 39 |
37 38
|
sylbir |
⊢ ( ( ( 𝐹 ‘ 𝑞 ) ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ) → ( 𝐹 ‘ 𝑞 ) ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ) |
| 40 |
35 39
|
sylan |
⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 𝑇 𝑝 ) ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ) → ( 𝐹 ‘ 𝑞 ) ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ) |
| 41 |
|
fvex |
⊢ ( 𝐹 ‘ 𝑞 ) ∈ V |
| 42 |
41
|
elsn |
⊢ ( ( 𝐹 ‘ 𝑞 ) ∈ { ( 𝐹 ‘ 𝑝 ) } ↔ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑝 ) ) |
| 43 |
|
elun2 |
⊢ ( ( 𝐹 ‘ 𝑞 ) ∈ { ( 𝐹 ‘ 𝑝 ) } → ( 𝐹 ‘ 𝑞 ) ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ) |
| 44 |
42 43
|
sylbir |
⊢ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑝 ) → ( 𝐹 ‘ 𝑞 ) ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ) |
| 45 |
44
|
ad2antrl |
⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 𝑇 𝑝 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) → ( 𝐹 ‘ 𝑞 ) ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ) |
| 46 |
1 2
|
weiunlem1 |
⊢ ( 𝑞 𝑇 𝑝 ↔ ( ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) ) ) |
| 47 |
46
|
simprbi |
⊢ ( 𝑞 𝑇 𝑝 → ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) ) |
| 48 |
47
|
3ad2ant3 |
⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 𝑇 𝑝 ) → ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) ) |
| 49 |
40 45 48
|
mpjaodan |
⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 𝑇 𝑝 ) → ( 𝐹 ‘ 𝑞 ) ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ) |
| 50 |
|
id |
⊢ ( 𝑡 = 𝑞 → 𝑡 = 𝑞 ) |
| 51 |
|
fveq2 |
⊢ ( 𝑡 = 𝑞 → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑞 ) ) |
| 52 |
51
|
csbeq1d |
⊢ ( 𝑡 = 𝑞 → ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 ) |
| 53 |
50 52
|
eleq12d |
⊢ ( 𝑡 = 𝑞 → ( 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 ↔ 𝑞 ∈ ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 ) ) |
| 54 |
5
|
simp2d |
⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ∀ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 ) |
| 55 |
54
|
3ad2ant1 |
⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 𝑇 𝑝 ) → ∀ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 ) |
| 56 |
53 55 34
|
rspcdva |
⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 𝑇 𝑝 ) → 𝑞 ∈ ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 ) |
| 57 |
|
csbeq1 |
⊢ ( 𝑠 = ( 𝐹 ‘ 𝑞 ) → ⦋ 𝑠 / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 ) |
| 58 |
57
|
eliuni |
⊢ ( ( ( 𝐹 ‘ 𝑞 ) ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ∧ 𝑞 ∈ ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 ) → 𝑞 ∈ ∪ 𝑠 ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ) |
| 59 |
49 56 58
|
syl2anc |
⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 𝑇 𝑝 ) → 𝑞 ∈ ∪ 𝑠 ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ) |
| 60 |
59
|
rabssdv |
⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → { 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∣ 𝑞 𝑇 𝑝 } ⊆ ∪ 𝑠 ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ) |
| 61 |
32 60
|
ssexd |
⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → { 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∣ 𝑞 𝑇 𝑝 } ∈ V ) |
| 62 |
61
|
ralrimiva |
⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) → ∀ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 { 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∣ 𝑞 𝑇 𝑝 } ∈ V ) |
| 63 |
|
df-se |
⊢ ( 𝑇 Se ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 { 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∣ 𝑞 𝑇 𝑝 } ∈ V ) |
| 64 |
62 63
|
sylibr |
⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) → 𝑇 Se ∪ 𝑥 ∈ 𝐴 𝐵 ) |