Step |
Hyp |
Ref |
Expression |
1 |
|
aomclem2.b |
⊢ 𝐵 = { 〈 𝑎 , 𝑏 〉 ∣ ∃ 𝑐 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( ( 𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎 ) ∧ ∀ 𝑑 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( 𝑑 ( 𝑧 ‘ ∪ dom 𝑧 ) 𝑐 → ( 𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏 ) ) ) } |
2 |
|
aomclem2.c |
⊢ 𝐶 = ( 𝑎 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) ) |
3 |
|
aomclem2.on |
⊢ ( 𝜑 → dom 𝑧 ∈ On ) |
4 |
|
aomclem2.su |
⊢ ( 𝜑 → dom 𝑧 = suc ∪ dom 𝑧 ) |
5 |
|
aomclem2.we |
⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ) |
6 |
|
aomclem2.a |
⊢ ( 𝜑 → 𝐴 ∈ On ) |
7 |
|
aomclem2.za |
⊢ ( 𝜑 → dom 𝑧 ⊆ 𝐴 ) |
8 |
|
aomclem2.y |
⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) ) |
9 |
|
vex |
⊢ 𝑎 ∈ V |
10 |
3 6
|
jca |
⊢ ( 𝜑 → ( dom 𝑧 ∈ On ∧ 𝐴 ∈ On ) ) |
11 |
|
r1ord3 |
⊢ ( ( dom 𝑧 ∈ On ∧ 𝐴 ∈ On ) → ( dom 𝑧 ⊆ 𝐴 → ( 𝑅1 ‘ dom 𝑧 ) ⊆ ( 𝑅1 ‘ 𝐴 ) ) ) |
12 |
10 7 11
|
sylc |
⊢ ( 𝜑 → ( 𝑅1 ‘ dom 𝑧 ) ⊆ ( 𝑅1 ‘ 𝐴 ) ) |
13 |
12
|
sspwd |
⊢ ( 𝜑 → 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ⊆ 𝒫 ( 𝑅1 ‘ 𝐴 ) ) |
14 |
13
|
sseld |
⊢ ( 𝜑 → ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) → 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ) ) |
15 |
|
rsp |
⊢ ( ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) → ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) → ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) ) ) |
16 |
8 14 15
|
sylsyld |
⊢ ( 𝜑 → ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) → ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) ) ) |
17 |
16
|
3imp |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) |
18 |
17
|
eldifad |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝑦 ‘ 𝑎 ) ∈ ( 𝒫 𝑎 ∩ Fin ) ) |
19 |
|
inss1 |
⊢ ( 𝒫 𝑎 ∩ Fin ) ⊆ 𝒫 𝑎 |
20 |
19
|
sseli |
⊢ ( ( 𝑦 ‘ 𝑎 ) ∈ ( 𝒫 𝑎 ∩ Fin ) → ( 𝑦 ‘ 𝑎 ) ∈ 𝒫 𝑎 ) |
21 |
20
|
elpwid |
⊢ ( ( 𝑦 ‘ 𝑎 ) ∈ ( 𝒫 𝑎 ∩ Fin ) → ( 𝑦 ‘ 𝑎 ) ⊆ 𝑎 ) |
22 |
18 21
|
syl |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝑦 ‘ 𝑎 ) ⊆ 𝑎 ) |
23 |
1 3 4 5
|
aomclem1 |
⊢ ( 𝜑 → 𝐵 Or ( 𝑅1 ‘ dom 𝑧 ) ) |
24 |
23
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → 𝐵 Or ( 𝑅1 ‘ dom 𝑧 ) ) |
25 |
|
inss2 |
⊢ ( 𝒫 𝑎 ∩ Fin ) ⊆ Fin |
26 |
25 18
|
sseldi |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝑦 ‘ 𝑎 ) ∈ Fin ) |
27 |
|
eldifsni |
⊢ ( ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) → ( 𝑦 ‘ 𝑎 ) ≠ ∅ ) |
28 |
17 27
|
syl |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝑦 ‘ 𝑎 ) ≠ ∅ ) |
29 |
|
elpwi |
⊢ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) → 𝑎 ⊆ ( 𝑅1 ‘ dom 𝑧 ) ) |
30 |
29
|
3ad2ant2 |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → 𝑎 ⊆ ( 𝑅1 ‘ dom 𝑧 ) ) |
31 |
22 30
|
sstrd |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝑦 ‘ 𝑎 ) ⊆ ( 𝑅1 ‘ dom 𝑧 ) ) |
32 |
|
fisupcl |
⊢ ( ( 𝐵 Or ( 𝑅1 ‘ dom 𝑧 ) ∧ ( ( 𝑦 ‘ 𝑎 ) ∈ Fin ∧ ( 𝑦 ‘ 𝑎 ) ≠ ∅ ∧ ( 𝑦 ‘ 𝑎 ) ⊆ ( 𝑅1 ‘ dom 𝑧 ) ) ) → sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) ∈ ( 𝑦 ‘ 𝑎 ) ) |
33 |
24 26 28 31 32
|
syl13anc |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) ∈ ( 𝑦 ‘ 𝑎 ) ) |
34 |
22 33
|
sseldd |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) ∈ 𝑎 ) |
35 |
2
|
fvmpt2 |
⊢ ( ( 𝑎 ∈ V ∧ sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) ∈ 𝑎 ) → ( 𝐶 ‘ 𝑎 ) = sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) ) |
36 |
9 34 35
|
sylancr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝐶 ‘ 𝑎 ) = sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) ) |
37 |
36 34
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝐶 ‘ 𝑎 ) ∈ 𝑎 ) |
38 |
37
|
3exp |
⊢ ( 𝜑 → ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) → ( 𝑎 ≠ ∅ → ( 𝐶 ‘ 𝑎 ) ∈ 𝑎 ) ) ) |
39 |
38
|
ralrimiv |
⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ( 𝑎 ≠ ∅ → ( 𝐶 ‘ 𝑎 ) ∈ 𝑎 ) ) |