Step |
Hyp |
Ref |
Expression |
1 |
|
fpwwe.1 |
⊢ 𝑊 = { 〈 𝑥 , 𝑟 〉 ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) } |
2 |
|
fpwwe.2 |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
3 |
|
fpwwe.3 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ dom card ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ) |
4 |
|
fpwwe.4 |
⊢ 𝑋 = ∪ dom 𝑊 |
5 |
|
df-ov |
⊢ ( 𝑌 ( 𝐹 ∘ 1st ) 𝑅 ) = ( ( 𝐹 ∘ 1st ) ‘ 〈 𝑌 , 𝑅 〉 ) |
6 |
|
fo1st |
⊢ 1st : V –onto→ V |
7 |
|
fofn |
⊢ ( 1st : V –onto→ V → 1st Fn V ) |
8 |
6 7
|
ax-mp |
⊢ 1st Fn V |
9 |
|
opex |
⊢ 〈 𝑌 , 𝑅 〉 ∈ V |
10 |
|
fvco2 |
⊢ ( ( 1st Fn V ∧ 〈 𝑌 , 𝑅 〉 ∈ V ) → ( ( 𝐹 ∘ 1st ) ‘ 〈 𝑌 , 𝑅 〉 ) = ( 𝐹 ‘ ( 1st ‘ 〈 𝑌 , 𝑅 〉 ) ) ) |
11 |
8 9 10
|
mp2an |
⊢ ( ( 𝐹 ∘ 1st ) ‘ 〈 𝑌 , 𝑅 〉 ) = ( 𝐹 ‘ ( 1st ‘ 〈 𝑌 , 𝑅 〉 ) ) |
12 |
5 11
|
eqtri |
⊢ ( 𝑌 ( 𝐹 ∘ 1st ) 𝑅 ) = ( 𝐹 ‘ ( 1st ‘ 〈 𝑌 , 𝑅 〉 ) ) |
13 |
1
|
bropaex12 |
⊢ ( 𝑌 𝑊 𝑅 → ( 𝑌 ∈ V ∧ 𝑅 ∈ V ) ) |
14 |
|
op1stg |
⊢ ( ( 𝑌 ∈ V ∧ 𝑅 ∈ V ) → ( 1st ‘ 〈 𝑌 , 𝑅 〉 ) = 𝑌 ) |
15 |
13 14
|
syl |
⊢ ( 𝑌 𝑊 𝑅 → ( 1st ‘ 〈 𝑌 , 𝑅 〉 ) = 𝑌 ) |
16 |
15
|
fveq2d |
⊢ ( 𝑌 𝑊 𝑅 → ( 𝐹 ‘ ( 1st ‘ 〈 𝑌 , 𝑅 〉 ) ) = ( 𝐹 ‘ 𝑌 ) ) |
17 |
12 16
|
eqtrid |
⊢ ( 𝑌 𝑊 𝑅 → ( 𝑌 ( 𝐹 ∘ 1st ) 𝑅 ) = ( 𝐹 ‘ 𝑌 ) ) |
18 |
17
|
eleq1d |
⊢ ( 𝑌 𝑊 𝑅 → ( ( 𝑌 ( 𝐹 ∘ 1st ) 𝑅 ) ∈ 𝑌 ↔ ( 𝐹 ‘ 𝑌 ) ∈ 𝑌 ) ) |
19 |
18
|
pm5.32i |
⊢ ( ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 ( 𝐹 ∘ 1st ) 𝑅 ) ∈ 𝑌 ) ↔ ( 𝑌 𝑊 𝑅 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑌 ) ) |
20 |
|
vex |
⊢ 𝑟 ∈ V |
21 |
20
|
cnvex |
⊢ ◡ 𝑟 ∈ V |
22 |
21
|
imaex |
⊢ ( ◡ 𝑟 “ { 𝑦 } ) ∈ V |
23 |
|
vex |
⊢ 𝑢 ∈ V |
24 |
20
|
inex1 |
⊢ ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ∈ V |
25 |
23 24
|
algrflem |
⊢ ( 𝑢 ( 𝐹 ∘ 1st ) ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = ( 𝐹 ‘ 𝑢 ) |
26 |
|
fveq2 |
⊢ ( 𝑢 = ( ◡ 𝑟 “ { 𝑦 } ) → ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) ) |
27 |
25 26
|
eqtrid |
⊢ ( 𝑢 = ( ◡ 𝑟 “ { 𝑦 } ) → ( 𝑢 ( 𝐹 ∘ 1st ) ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = ( 𝐹 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) ) |
28 |
27
|
eqeq1d |
⊢ ( 𝑢 = ( ◡ 𝑟 “ { 𝑦 } ) → ( ( 𝑢 ( 𝐹 ∘ 1st ) ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ ( 𝐹 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) |
29 |
22 28
|
sbcie |
⊢ ( [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 ( 𝐹 ∘ 1st ) ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ ( 𝐹 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) |
30 |
29
|
ralbii |
⊢ ( ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 ( 𝐹 ∘ 1st ) ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) |
31 |
30
|
anbi2i |
⊢ ( ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 ( 𝐹 ∘ 1st ) ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ↔ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) |
32 |
31
|
anbi2i |
⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 ( 𝐹 ∘ 1st ) ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) ) |
33 |
32
|
opabbii |
⊢ { 〈 𝑥 , 𝑟 〉 ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 ( 𝐹 ∘ 1st ) ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) } = { 〈 𝑥 , 𝑟 〉 ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) } |
34 |
1 33
|
eqtr4i |
⊢ 𝑊 = { 〈 𝑥 , 𝑟 〉 ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 ( 𝐹 ∘ 1st ) ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) } |
35 |
|
vex |
⊢ 𝑥 ∈ V |
36 |
35 20
|
algrflem |
⊢ ( 𝑥 ( 𝐹 ∘ 1st ) 𝑟 ) = ( 𝐹 ‘ 𝑥 ) |
37 |
|
simp1 |
⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → 𝑥 ⊆ 𝐴 ) |
38 |
|
velpw |
⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 ) |
39 |
37 38
|
sylibr |
⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → 𝑥 ∈ 𝒫 𝐴 ) |
40 |
|
19.8a |
⊢ ( 𝑟 We 𝑥 → ∃ 𝑟 𝑟 We 𝑥 ) |
41 |
40
|
3ad2ant3 |
⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → ∃ 𝑟 𝑟 We 𝑥 ) |
42 |
|
ween |
⊢ ( 𝑥 ∈ dom card ↔ ∃ 𝑟 𝑟 We 𝑥 ) |
43 |
41 42
|
sylibr |
⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → 𝑥 ∈ dom card ) |
44 |
39 43
|
elind |
⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → 𝑥 ∈ ( 𝒫 𝐴 ∩ dom card ) ) |
45 |
44 3
|
sylan2 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ) |
46 |
36 45
|
eqeltrid |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 ( 𝐹 ∘ 1st ) 𝑟 ) ∈ 𝐴 ) |
47 |
34 2 46 4
|
fpwwe2 |
⊢ ( 𝜑 → ( ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 ( 𝐹 ∘ 1st ) 𝑅 ) ∈ 𝑌 ) ↔ ( 𝑌 = 𝑋 ∧ 𝑅 = ( 𝑊 ‘ 𝑋 ) ) ) ) |
48 |
19 47
|
bitr3id |
⊢ ( 𝜑 → ( ( 𝑌 𝑊 𝑅 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑌 ) ↔ ( 𝑌 = 𝑋 ∧ 𝑅 = ( 𝑊 ‘ 𝑋 ) ) ) ) |