Step |
Hyp |
Ref |
Expression |
1 |
|
mpct.a |
⊢ ( 𝜑 → 𝐴 ≼ ω ) |
2 |
|
mpct.b |
⊢ ( 𝜑 → 𝐵 ∈ Fin ) |
3 |
|
oveq2 |
⊢ ( 𝑥 = ∅ → ( 𝐴 ↑m 𝑥 ) = ( 𝐴 ↑m ∅ ) ) |
4 |
3
|
breq1d |
⊢ ( 𝑥 = ∅ → ( ( 𝐴 ↑m 𝑥 ) ≼ ω ↔ ( 𝐴 ↑m ∅ ) ≼ ω ) ) |
5 |
|
oveq2 |
⊢ ( 𝑥 = 𝑦 → ( 𝐴 ↑m 𝑥 ) = ( 𝐴 ↑m 𝑦 ) ) |
6 |
5
|
breq1d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ↑m 𝑥 ) ≼ ω ↔ ( 𝐴 ↑m 𝑦 ) ≼ ω ) ) |
7 |
|
oveq2 |
⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝐴 ↑m 𝑥 ) = ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ) |
8 |
7
|
breq1d |
⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝐴 ↑m 𝑥 ) ≼ ω ↔ ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ≼ ω ) ) |
9 |
|
oveq2 |
⊢ ( 𝑥 = 𝐵 → ( 𝐴 ↑m 𝑥 ) = ( 𝐴 ↑m 𝐵 ) ) |
10 |
9
|
breq1d |
⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ↑m 𝑥 ) ≼ ω ↔ ( 𝐴 ↑m 𝐵 ) ≼ ω ) ) |
11 |
|
ctex |
⊢ ( 𝐴 ≼ ω → 𝐴 ∈ V ) |
12 |
1 11
|
syl |
⊢ ( 𝜑 → 𝐴 ∈ V ) |
13 |
|
mapdm0 |
⊢ ( 𝐴 ∈ V → ( 𝐴 ↑m ∅ ) = { ∅ } ) |
14 |
12 13
|
syl |
⊢ ( 𝜑 → ( 𝐴 ↑m ∅ ) = { ∅ } ) |
15 |
|
snfi |
⊢ { ∅ } ∈ Fin |
16 |
|
fict |
⊢ ( { ∅ } ∈ Fin → { ∅ } ≼ ω ) |
17 |
15 16
|
ax-mp |
⊢ { ∅ } ≼ ω |
18 |
17
|
a1i |
⊢ ( 𝜑 → { ∅ } ≼ ω ) |
19 |
14 18
|
eqbrtrd |
⊢ ( 𝜑 → ( 𝐴 ↑m ∅ ) ≼ ω ) |
20 |
|
vex |
⊢ 𝑦 ∈ V |
21 |
20
|
a1i |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) ) ) ∧ ( 𝐴 ↑m 𝑦 ) ≼ ω ) → 𝑦 ∈ V ) |
22 |
|
snex |
⊢ { 𝑧 } ∈ V |
23 |
22
|
a1i |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) ) ) ∧ ( 𝐴 ↑m 𝑦 ) ≼ ω ) → { 𝑧 } ∈ V ) |
24 |
12
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) ) ) ∧ ( 𝐴 ↑m 𝑦 ) ≼ ω ) → 𝐴 ∈ V ) |
25 |
|
eldifn |
⊢ ( 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) → ¬ 𝑧 ∈ 𝑦 ) |
26 |
|
disjsn |
⊢ ( ( 𝑦 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ 𝑦 ) |
27 |
25 26
|
sylibr |
⊢ ( 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) → ( 𝑦 ∩ { 𝑧 } ) = ∅ ) |
28 |
27
|
adantl |
⊢ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) ) → ( 𝑦 ∩ { 𝑧 } ) = ∅ ) |
29 |
28
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) ) ) ∧ ( 𝐴 ↑m 𝑦 ) ≼ ω ) → ( 𝑦 ∩ { 𝑧 } ) = ∅ ) |
30 |
|
mapunen |
⊢ ( ( ( 𝑦 ∈ V ∧ { 𝑧 } ∈ V ∧ 𝐴 ∈ V ) ∧ ( 𝑦 ∩ { 𝑧 } ) = ∅ ) → ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ≈ ( ( 𝐴 ↑m 𝑦 ) × ( 𝐴 ↑m { 𝑧 } ) ) ) |
31 |
21 23 24 29 30
|
syl31anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) ) ) ∧ ( 𝐴 ↑m 𝑦 ) ≼ ω ) → ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ≈ ( ( 𝐴 ↑m 𝑦 ) × ( 𝐴 ↑m { 𝑧 } ) ) ) |
32 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) ) ) ∧ ( 𝐴 ↑m 𝑦 ) ≼ ω ) → ( 𝐴 ↑m 𝑦 ) ≼ ω ) |
33 |
|
vex |
⊢ 𝑧 ∈ V |
34 |
33
|
a1i |
⊢ ( 𝜑 → 𝑧 ∈ V ) |
35 |
12 34
|
mapsnend |
⊢ ( 𝜑 → ( 𝐴 ↑m { 𝑧 } ) ≈ 𝐴 ) |
36 |
|
endomtr |
⊢ ( ( ( 𝐴 ↑m { 𝑧 } ) ≈ 𝐴 ∧ 𝐴 ≼ ω ) → ( 𝐴 ↑m { 𝑧 } ) ≼ ω ) |
37 |
35 1 36
|
syl2anc |
⊢ ( 𝜑 → ( 𝐴 ↑m { 𝑧 } ) ≼ ω ) |
38 |
37
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) ) ) ∧ ( 𝐴 ↑m 𝑦 ) ≼ ω ) → ( 𝐴 ↑m { 𝑧 } ) ≼ ω ) |
39 |
|
xpct |
⊢ ( ( ( 𝐴 ↑m 𝑦 ) ≼ ω ∧ ( 𝐴 ↑m { 𝑧 } ) ≼ ω ) → ( ( 𝐴 ↑m 𝑦 ) × ( 𝐴 ↑m { 𝑧 } ) ) ≼ ω ) |
40 |
32 38 39
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) ) ) ∧ ( 𝐴 ↑m 𝑦 ) ≼ ω ) → ( ( 𝐴 ↑m 𝑦 ) × ( 𝐴 ↑m { 𝑧 } ) ) ≼ ω ) |
41 |
|
endomtr |
⊢ ( ( ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ≈ ( ( 𝐴 ↑m 𝑦 ) × ( 𝐴 ↑m { 𝑧 } ) ) ∧ ( ( 𝐴 ↑m 𝑦 ) × ( 𝐴 ↑m { 𝑧 } ) ) ≼ ω ) → ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ≼ ω ) |
42 |
31 40 41
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) ) ) ∧ ( 𝐴 ↑m 𝑦 ) ≼ ω ) → ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ≼ ω ) |
43 |
42
|
ex |
⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) ) ) → ( ( 𝐴 ↑m 𝑦 ) ≼ ω → ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ≼ ω ) ) |
44 |
4 6 8 10 19 43 2
|
findcard2d |
⊢ ( 𝜑 → ( 𝐴 ↑m 𝐵 ) ≼ ω ) |