Step |
Hyp |
Ref |
Expression |
1 |
|
aomclem6.b |
⊢ 𝐵 = { 〈 𝑎 , 𝑏 〉 ∣ ∃ 𝑐 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( ( 𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎 ) ∧ ∀ 𝑑 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( 𝑑 ( 𝑧 ‘ ∪ dom 𝑧 ) 𝑐 → ( 𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏 ) ) ) } |
2 |
|
aomclem6.c |
⊢ 𝐶 = ( 𝑎 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) ) |
3 |
|
aomclem6.d |
⊢ 𝐷 = recs ( ( 𝑎 ∈ V ↦ ( 𝐶 ‘ ( ( 𝑅1 ‘ dom 𝑧 ) ∖ ran 𝑎 ) ) ) ) |
4 |
|
aomclem6.e |
⊢ 𝐸 = { 〈 𝑎 , 𝑏 〉 ∣ ∩ ( ◡ 𝐷 “ { 𝑎 } ) ∈ ∩ ( ◡ 𝐷 “ { 𝑏 } ) } |
5 |
|
aomclem6.f |
⊢ 𝐹 = { 〈 𝑎 , 𝑏 〉 ∣ ( ( rank ‘ 𝑎 ) E ( rank ‘ 𝑏 ) ∨ ( ( rank ‘ 𝑎 ) = ( rank ‘ 𝑏 ) ∧ 𝑎 ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) 𝑏 ) ) } |
6 |
|
aomclem6.g |
⊢ 𝐺 = ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) ∩ ( ( 𝑅1 ‘ dom 𝑧 ) × ( 𝑅1 ‘ dom 𝑧 ) ) ) |
7 |
|
aomclem6.h |
⊢ 𝐻 = recs ( ( 𝑧 ∈ V ↦ 𝐺 ) ) |
8 |
|
aomclem6.a |
⊢ ( 𝜑 → 𝐴 ∈ On ) |
9 |
|
aomclem6.y |
⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) ) |
10 |
|
ssid |
⊢ 𝐴 ⊆ 𝐴 |
11 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝐴 ⊆ 𝐴 ) → 𝐴 ∈ On ) |
12 |
|
sseq1 |
⊢ ( 𝑐 = 𝑑 → ( 𝑐 ⊆ 𝐴 ↔ 𝑑 ⊆ 𝐴 ) ) |
13 |
12
|
anbi2d |
⊢ ( 𝑐 = 𝑑 → ( ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ↔ ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) ) ) |
14 |
|
fveq2 |
⊢ ( 𝑐 = 𝑑 → ( 𝐻 ‘ 𝑐 ) = ( 𝐻 ‘ 𝑑 ) ) |
15 |
|
fveq2 |
⊢ ( 𝑐 = 𝑑 → ( 𝑅1 ‘ 𝑐 ) = ( 𝑅1 ‘ 𝑑 ) ) |
16 |
14 15
|
weeq12d |
⊢ ( 𝑐 = 𝑑 → ( ( 𝐻 ‘ 𝑐 ) We ( 𝑅1 ‘ 𝑐 ) ↔ ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ) |
17 |
13 16
|
imbi12d |
⊢ ( 𝑐 = 𝑑 → ( ( ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑐 ) We ( 𝑅1 ‘ 𝑐 ) ) ↔ ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ) ) |
18 |
|
sseq1 |
⊢ ( 𝑐 = 𝐴 → ( 𝑐 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴 ) ) |
19 |
18
|
anbi2d |
⊢ ( 𝑐 = 𝐴 → ( ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ↔ ( 𝜑 ∧ 𝐴 ⊆ 𝐴 ) ) ) |
20 |
|
fveq2 |
⊢ ( 𝑐 = 𝐴 → ( 𝐻 ‘ 𝑐 ) = ( 𝐻 ‘ 𝐴 ) ) |
21 |
|
fveq2 |
⊢ ( 𝑐 = 𝐴 → ( 𝑅1 ‘ 𝑐 ) = ( 𝑅1 ‘ 𝐴 ) ) |
22 |
20 21
|
weeq12d |
⊢ ( 𝑐 = 𝐴 → ( ( 𝐻 ‘ 𝑐 ) We ( 𝑅1 ‘ 𝑐 ) ↔ ( 𝐻 ‘ 𝐴 ) We ( 𝑅1 ‘ 𝐴 ) ) ) |
23 |
19 22
|
imbi12d |
⊢ ( 𝑐 = 𝐴 → ( ( ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑐 ) We ( 𝑅1 ‘ 𝑐 ) ) ↔ ( ( 𝜑 ∧ 𝐴 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝐴 ) We ( 𝑅1 ‘ 𝐴 ) ) ) ) |
24 |
|
dmeq |
⊢ ( 𝑧 = ( 𝐻 ↾ 𝑐 ) → dom 𝑧 = dom ( 𝐻 ↾ 𝑐 ) ) |
25 |
24
|
adantl |
⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → dom 𝑧 = dom ( 𝐻 ↾ 𝑐 ) ) |
26 |
|
simpl1 |
⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → 𝑐 ∈ On ) |
27 |
|
onss |
⊢ ( 𝑐 ∈ On → 𝑐 ⊆ On ) |
28 |
7
|
tfr1 |
⊢ 𝐻 Fn On |
29 |
|
fnssres |
⊢ ( ( 𝐻 Fn On ∧ 𝑐 ⊆ On ) → ( 𝐻 ↾ 𝑐 ) Fn 𝑐 ) |
30 |
28 29
|
mpan |
⊢ ( 𝑐 ⊆ On → ( 𝐻 ↾ 𝑐 ) Fn 𝑐 ) |
31 |
|
fndm |
⊢ ( ( 𝐻 ↾ 𝑐 ) Fn 𝑐 → dom ( 𝐻 ↾ 𝑐 ) = 𝑐 ) |
32 |
26 27 30 31
|
4syl |
⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → dom ( 𝐻 ↾ 𝑐 ) = 𝑐 ) |
33 |
25 32
|
eqtrd |
⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → dom 𝑧 = 𝑐 ) |
34 |
33 26
|
eqeltrd |
⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → dom 𝑧 ∈ On ) |
35 |
33
|
eleq2d |
⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → ( 𝑎 ∈ dom 𝑧 ↔ 𝑎 ∈ 𝑐 ) ) |
36 |
35
|
biimpa |
⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → 𝑎 ∈ 𝑐 ) |
37 |
|
simpll2 |
⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ) |
38 |
|
simpl3l |
⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → 𝜑 ) |
39 |
38
|
adantr |
⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → 𝜑 ) |
40 |
|
onelss |
⊢ ( dom 𝑧 ∈ On → ( 𝑎 ∈ dom 𝑧 → 𝑎 ⊆ dom 𝑧 ) ) |
41 |
34 40
|
syl |
⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → ( 𝑎 ∈ dom 𝑧 → 𝑎 ⊆ dom 𝑧 ) ) |
42 |
41
|
imp |
⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → 𝑎 ⊆ dom 𝑧 ) |
43 |
|
simpl3r |
⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → 𝑐 ⊆ 𝐴 ) |
44 |
33 43
|
eqsstrd |
⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → dom 𝑧 ⊆ 𝐴 ) |
45 |
44
|
adantr |
⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → dom 𝑧 ⊆ 𝐴 ) |
46 |
42 45
|
sstrd |
⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → 𝑎 ⊆ 𝐴 ) |
47 |
|
sseq1 |
⊢ ( 𝑑 = 𝑎 → ( 𝑑 ⊆ 𝐴 ↔ 𝑎 ⊆ 𝐴 ) ) |
48 |
47
|
anbi2d |
⊢ ( 𝑑 = 𝑎 → ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) ↔ ( 𝜑 ∧ 𝑎 ⊆ 𝐴 ) ) ) |
49 |
|
fveq2 |
⊢ ( 𝑑 = 𝑎 → ( 𝐻 ‘ 𝑑 ) = ( 𝐻 ‘ 𝑎 ) ) |
50 |
|
fveq2 |
⊢ ( 𝑑 = 𝑎 → ( 𝑅1 ‘ 𝑑 ) = ( 𝑅1 ‘ 𝑎 ) ) |
51 |
49 50
|
weeq12d |
⊢ ( 𝑑 = 𝑎 → ( ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ↔ ( 𝐻 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ) ) |
52 |
48 51
|
imbi12d |
⊢ ( 𝑑 = 𝑎 → ( ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ↔ ( ( 𝜑 ∧ 𝑎 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ) ) ) |
53 |
52
|
rspcva |
⊢ ( ( 𝑎 ∈ 𝑐 ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ) → ( ( 𝜑 ∧ 𝑎 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ) ) |
54 |
53
|
imp |
⊢ ( ( ( 𝑎 ∈ 𝑐 ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ) ∧ ( 𝜑 ∧ 𝑎 ⊆ 𝐴 ) ) → ( 𝐻 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ) |
55 |
36 37 39 46 54
|
syl22anc |
⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → ( 𝐻 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ) |
56 |
|
fveq1 |
⊢ ( 𝑧 = ( 𝐻 ↾ 𝑐 ) → ( 𝑧 ‘ 𝑎 ) = ( ( 𝐻 ↾ 𝑐 ) ‘ 𝑎 ) ) |
57 |
56
|
ad2antlr |
⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → ( 𝑧 ‘ 𝑎 ) = ( ( 𝐻 ↾ 𝑐 ) ‘ 𝑎 ) ) |
58 |
|
fvres |
⊢ ( 𝑎 ∈ 𝑐 → ( ( 𝐻 ↾ 𝑐 ) ‘ 𝑎 ) = ( 𝐻 ‘ 𝑎 ) ) |
59 |
36 58
|
syl |
⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → ( ( 𝐻 ↾ 𝑐 ) ‘ 𝑎 ) = ( 𝐻 ‘ 𝑎 ) ) |
60 |
57 59
|
eqtrd |
⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → ( 𝑧 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑎 ) ) |
61 |
|
weeq1 |
⊢ ( ( 𝑧 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑎 ) → ( ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ↔ ( 𝐻 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ) ) |
62 |
60 61
|
syl |
⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → ( ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ↔ ( 𝐻 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ) ) |
63 |
55 62
|
mpbird |
⊢ ( ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) ∧ 𝑎 ∈ dom 𝑧 ) → ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ) |
64 |
63
|
ralrimiva |
⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ) |
65 |
38 8
|
syl |
⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → 𝐴 ∈ On ) |
66 |
38 9
|
syl |
⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) ) |
67 |
1 2 3 4 5 6 34 64 65 44 66
|
aomclem5 |
⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → 𝐺 We ( 𝑅1 ‘ dom 𝑧 ) ) |
68 |
33
|
fveq2d |
⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → ( 𝑅1 ‘ dom 𝑧 ) = ( 𝑅1 ‘ 𝑐 ) ) |
69 |
|
weeq2 |
⊢ ( ( 𝑅1 ‘ dom 𝑧 ) = ( 𝑅1 ‘ 𝑐 ) → ( 𝐺 We ( 𝑅1 ‘ dom 𝑧 ) ↔ 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) ) |
70 |
68 69
|
syl |
⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → ( 𝐺 We ( 𝑅1 ‘ dom 𝑧 ) ↔ 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) ) |
71 |
67 70
|
mpbid |
⊢ ( ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) ∧ 𝑧 = ( 𝐻 ↾ 𝑐 ) ) → 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) |
72 |
71
|
ex |
⊢ ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) → ( 𝑧 = ( 𝐻 ↾ 𝑐 ) → 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) ) |
73 |
72
|
alrimiv |
⊢ ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) → ∀ 𝑧 ( 𝑧 = ( 𝐻 ↾ 𝑐 ) → 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) ) |
74 |
|
nfv |
⊢ Ⅎ 𝑑 ( 𝑧 = ( 𝐻 ↾ 𝑐 ) → 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) |
75 |
|
nfv |
⊢ Ⅎ 𝑧 𝑑 = ( 𝐻 ↾ 𝑐 ) |
76 |
|
nfsbc1v |
⊢ Ⅎ 𝑧 [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) |
77 |
75 76
|
nfim |
⊢ Ⅎ 𝑧 ( 𝑑 = ( 𝐻 ↾ 𝑐 ) → [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) |
78 |
|
eqeq1 |
⊢ ( 𝑧 = 𝑑 → ( 𝑧 = ( 𝐻 ↾ 𝑐 ) ↔ 𝑑 = ( 𝐻 ↾ 𝑐 ) ) ) |
79 |
|
sbceq1a |
⊢ ( 𝑧 = 𝑑 → ( 𝐺 We ( 𝑅1 ‘ 𝑐 ) ↔ [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) ) |
80 |
78 79
|
imbi12d |
⊢ ( 𝑧 = 𝑑 → ( ( 𝑧 = ( 𝐻 ↾ 𝑐 ) → 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) ↔ ( 𝑑 = ( 𝐻 ↾ 𝑐 ) → [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) ) ) |
81 |
74 77 80
|
cbvalv1 |
⊢ ( ∀ 𝑧 ( 𝑧 = ( 𝐻 ↾ 𝑐 ) → 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) ↔ ∀ 𝑑 ( 𝑑 = ( 𝐻 ↾ 𝑐 ) → [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) ) |
82 |
73 81
|
sylib |
⊢ ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) → ∀ 𝑑 ( 𝑑 = ( 𝐻 ↾ 𝑐 ) → [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) ) |
83 |
|
nfsbc1v |
⊢ Ⅎ 𝑑 [ ( 𝐻 ↾ 𝑐 ) / 𝑑 ] [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) |
84 |
|
fnfun |
⊢ ( 𝐻 Fn On → Fun 𝐻 ) |
85 |
28 84
|
ax-mp |
⊢ Fun 𝐻 |
86 |
|
vex |
⊢ 𝑐 ∈ V |
87 |
|
resfunexg |
⊢ ( ( Fun 𝐻 ∧ 𝑐 ∈ V ) → ( 𝐻 ↾ 𝑐 ) ∈ V ) |
88 |
85 86 87
|
mp2an |
⊢ ( 𝐻 ↾ 𝑐 ) ∈ V |
89 |
|
sbceq1a |
⊢ ( 𝑑 = ( 𝐻 ↾ 𝑐 ) → ( [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ↔ [ ( 𝐻 ↾ 𝑐 ) / 𝑑 ] [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) ) |
90 |
83 88 89
|
ceqsal |
⊢ ( ∀ 𝑑 ( 𝑑 = ( 𝐻 ↾ 𝑐 ) → [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) ↔ [ ( 𝐻 ↾ 𝑐 ) / 𝑑 ] [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) |
91 |
82 90
|
sylib |
⊢ ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) → [ ( 𝐻 ↾ 𝑐 ) / 𝑑 ] [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) |
92 |
|
sbccow |
⊢ ( [ ( 𝐻 ↾ 𝑐 ) / 𝑑 ] [ 𝑑 / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ↔ [ ( 𝐻 ↾ 𝑐 ) / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) |
93 |
91 92
|
sylib |
⊢ ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) → [ ( 𝐻 ↾ 𝑐 ) / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) |
94 |
|
nfcsb1v |
⊢ Ⅎ 𝑧 ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 |
95 |
|
nfcv |
⊢ Ⅎ 𝑧 ( 𝑅1 ‘ 𝑐 ) |
96 |
94 95
|
nfwe |
⊢ Ⅎ 𝑧 ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 We ( 𝑅1 ‘ 𝑐 ) |
97 |
|
csbeq1a |
⊢ ( 𝑧 = ( 𝐻 ↾ 𝑐 ) → 𝐺 = ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 ) |
98 |
|
weeq1 |
⊢ ( 𝐺 = ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 → ( 𝐺 We ( 𝑅1 ‘ 𝑐 ) ↔ ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) ) |
99 |
97 98
|
syl |
⊢ ( 𝑧 = ( 𝐻 ↾ 𝑐 ) → ( 𝐺 We ( 𝑅1 ‘ 𝑐 ) ↔ ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) ) |
100 |
96 99
|
sbciegf |
⊢ ( ( 𝐻 ↾ 𝑐 ) ∈ V → ( [ ( 𝐻 ↾ 𝑐 ) / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ↔ ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) ) |
101 |
88 100
|
ax-mp |
⊢ ( [ ( 𝐻 ↾ 𝑐 ) / 𝑧 ] 𝐺 We ( 𝑅1 ‘ 𝑐 ) ↔ ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) |
102 |
93 101
|
sylib |
⊢ ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) → ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) |
103 |
|
recsval |
⊢ ( 𝑐 ∈ On → ( recs ( ( 𝑧 ∈ V ↦ 𝐺 ) ) ‘ 𝑐 ) = ( ( 𝑧 ∈ V ↦ 𝐺 ) ‘ ( recs ( ( 𝑧 ∈ V ↦ 𝐺 ) ) ↾ 𝑐 ) ) ) |
104 |
7
|
fveq1i |
⊢ ( 𝐻 ‘ 𝑐 ) = ( recs ( ( 𝑧 ∈ V ↦ 𝐺 ) ) ‘ 𝑐 ) |
105 |
|
fvex |
⊢ ( 𝑅1 ‘ dom 𝑧 ) ∈ V |
106 |
105 105
|
xpex |
⊢ ( ( 𝑅1 ‘ dom 𝑧 ) × ( 𝑅1 ‘ dom 𝑧 ) ) ∈ V |
107 |
106
|
inex2 |
⊢ ( if ( dom 𝑧 = ∪ dom 𝑧 , 𝐹 , 𝐸 ) ∩ ( ( 𝑅1 ‘ dom 𝑧 ) × ( 𝑅1 ‘ dom 𝑧 ) ) ) ∈ V |
108 |
6 107
|
eqeltri |
⊢ 𝐺 ∈ V |
109 |
108
|
csbex |
⊢ ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 ∈ V |
110 |
|
eqid |
⊢ ( 𝑧 ∈ V ↦ 𝐺 ) = ( 𝑧 ∈ V ↦ 𝐺 ) |
111 |
110
|
fvmpts |
⊢ ( ( ( 𝐻 ↾ 𝑐 ) ∈ V ∧ ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 ∈ V ) → ( ( 𝑧 ∈ V ↦ 𝐺 ) ‘ ( 𝐻 ↾ 𝑐 ) ) = ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 ) |
112 |
88 109 111
|
mp2an |
⊢ ( ( 𝑧 ∈ V ↦ 𝐺 ) ‘ ( 𝐻 ↾ 𝑐 ) ) = ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 |
113 |
7
|
reseq1i |
⊢ ( 𝐻 ↾ 𝑐 ) = ( recs ( ( 𝑧 ∈ V ↦ 𝐺 ) ) ↾ 𝑐 ) |
114 |
113
|
fveq2i |
⊢ ( ( 𝑧 ∈ V ↦ 𝐺 ) ‘ ( 𝐻 ↾ 𝑐 ) ) = ( ( 𝑧 ∈ V ↦ 𝐺 ) ‘ ( recs ( ( 𝑧 ∈ V ↦ 𝐺 ) ) ↾ 𝑐 ) ) |
115 |
112 114
|
eqtr3i |
⊢ ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 = ( ( 𝑧 ∈ V ↦ 𝐺 ) ‘ ( recs ( ( 𝑧 ∈ V ↦ 𝐺 ) ) ↾ 𝑐 ) ) |
116 |
103 104 115
|
3eqtr4g |
⊢ ( 𝑐 ∈ On → ( 𝐻 ‘ 𝑐 ) = ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 ) |
117 |
|
weeq1 |
⊢ ( ( 𝐻 ‘ 𝑐 ) = ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 → ( ( 𝐻 ‘ 𝑐 ) We ( 𝑅1 ‘ 𝑐 ) ↔ ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) ) |
118 |
116 117
|
syl |
⊢ ( 𝑐 ∈ On → ( ( 𝐻 ‘ 𝑐 ) We ( 𝑅1 ‘ 𝑐 ) ↔ ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) ) |
119 |
118
|
3ad2ant1 |
⊢ ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑐 ) We ( 𝑅1 ‘ 𝑐 ) ↔ ⦋ ( 𝐻 ↾ 𝑐 ) / 𝑧 ⦌ 𝐺 We ( 𝑅1 ‘ 𝑐 ) ) ) |
120 |
102 119
|
mpbird |
⊢ ( ( 𝑐 ∈ On ∧ ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) ∧ ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) ) → ( 𝐻 ‘ 𝑐 ) We ( 𝑅1 ‘ 𝑐 ) ) |
121 |
120
|
3exp |
⊢ ( 𝑐 ∈ On → ( ∀ 𝑑 ∈ 𝑐 ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) We ( 𝑅1 ‘ 𝑑 ) ) → ( ( 𝜑 ∧ 𝑐 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝑐 ) We ( 𝑅1 ‘ 𝑐 ) ) ) ) |
122 |
17 23 121
|
tfis3 |
⊢ ( 𝐴 ∈ On → ( ( 𝜑 ∧ 𝐴 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝐴 ) We ( 𝑅1 ‘ 𝐴 ) ) ) |
123 |
11 122
|
mpcom |
⊢ ( ( 𝜑 ∧ 𝐴 ⊆ 𝐴 ) → ( 𝐻 ‘ 𝐴 ) We ( 𝑅1 ‘ 𝐴 ) ) |
124 |
10 123
|
mpan2 |
⊢ ( 𝜑 → ( 𝐻 ‘ 𝐴 ) We ( 𝑅1 ‘ 𝐴 ) ) |