Step |
Hyp |
Ref |
Expression |
1 |
|
fpwwe2.1 |
⊢ 𝑊 = { 〈 𝑥 , 𝑟 〉 ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) } |
2 |
|
simpll |
⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) → 𝑥 ⊆ 𝐴 ) |
3 |
|
velpw |
⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 ) |
4 |
2 3
|
sylibr |
⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) → 𝑥 ∈ 𝒫 𝐴 ) |
5 |
|
simplr |
⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) → 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) |
6 |
|
xpss12 |
⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐴 ) → ( 𝑥 × 𝑥 ) ⊆ ( 𝐴 × 𝐴 ) ) |
7 |
2 2 6
|
syl2anc |
⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) → ( 𝑥 × 𝑥 ) ⊆ ( 𝐴 × 𝐴 ) ) |
8 |
5 7
|
sstrd |
⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) → 𝑟 ⊆ ( 𝐴 × 𝐴 ) ) |
9 |
|
velpw |
⊢ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ↔ 𝑟 ⊆ ( 𝐴 × 𝐴 ) ) |
10 |
8 9
|
sylibr |
⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) → 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ) |
11 |
4 10
|
jca |
⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) → ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ) ) |
12 |
11
|
ssopab2i |
⊢ { 〈 𝑥 , 𝑟 〉 ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) } ⊆ { 〈 𝑥 , 𝑟 〉 ∣ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ) } |
13 |
|
df-xp |
⊢ ( 𝒫 𝐴 × 𝒫 ( 𝐴 × 𝐴 ) ) = { 〈 𝑥 , 𝑟 〉 ∣ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ) } |
14 |
12 1 13
|
3sstr4i |
⊢ 𝑊 ⊆ ( 𝒫 𝐴 × 𝒫 ( 𝐴 × 𝐴 ) ) |