Proof of Theorem finxpreclem3
Step | Hyp | Ref
| Expression |
1 | | finxpreclem3.1 |
. . . 4
⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
2 | 1 | a1i 11 |
. . 3
⊢ (((𝑁 ∈ ω ∧
2o ⊆ 𝑁)
∧ 𝑋 ∈ (V ×
𝑈)) → 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))) |
3 | | eqeq1 2742 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (𝑛 = 1o ↔ 𝑁 = 1o)) |
4 | | eleq1 2826 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑥 ∈ 𝑈 ↔ 𝑋 ∈ 𝑈)) |
5 | 3, 4 | bi2anan9 636 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → ((𝑛 = 1o ∧ 𝑥 ∈ 𝑈) ↔ (𝑁 = 1o ∧ 𝑋 ∈ 𝑈))) |
6 | | eleq1 2826 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑥 ∈ (V × 𝑈) ↔ 𝑋 ∈ (V × 𝑈))) |
7 | 6 | adantl 482 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → (𝑥 ∈ (V × 𝑈) ↔ 𝑋 ∈ (V × 𝑈))) |
8 | | unieq 4850 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → ∪ 𝑛 = ∪
𝑁) |
9 | 8 | adantr 481 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → ∪ 𝑛 = ∪
𝑁) |
10 | | fveq2 6774 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (1st ‘𝑥) = (1st ‘𝑋)) |
11 | 10 | adantl 482 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → (1st ‘𝑥) = (1st ‘𝑋)) |
12 | 9, 11 | opeq12d 4812 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → 〈∪
𝑛, (1st
‘𝑥)〉 =
〈∪ 𝑁, (1st ‘𝑋)〉) |
13 | | opeq12 4806 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → 〈𝑛, 𝑥〉 = 〈𝑁, 𝑋〉) |
14 | 7, 12, 13 | ifbieq12d 4487 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = if(𝑋 ∈ (V × 𝑈), 〈∪ 𝑁, (1st ‘𝑋)〉, 〈𝑁, 𝑋〉)) |
15 | 5, 14 | ifbieq2d 4485 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = if((𝑁 = 1o ∧ 𝑋 ∈ 𝑈), ∅, if(𝑋 ∈ (V × 𝑈), 〈∪ 𝑁, (1st ‘𝑋)〉, 〈𝑁, 𝑋〉))) |
16 | | sssucid 6343 |
. . . . . . . . . . . . 13
⊢
1o ⊆ suc 1o |
17 | | df-2o 8298 |
. . . . . . . . . . . . 13
⊢
2o = suc 1o |
18 | 16, 17 | sseqtrri 3958 |
. . . . . . . . . . . 12
⊢
1o ⊆ 2o |
19 | | 1on 8309 |
. . . . . . . . . . . . . 14
⊢
1o ∈ On |
20 | 17, 19 | sucneqoni 35537 |
. . . . . . . . . . . . 13
⊢
2o ≠ 1o |
21 | 20 | necomi 2998 |
. . . . . . . . . . . 12
⊢
1o ≠ 2o |
22 | | df-pss 3906 |
. . . . . . . . . . . 12
⊢
(1o ⊊ 2o ↔ (1o ⊆
2o ∧ 1o ≠ 2o)) |
23 | 18, 21, 22 | mpbir2an 708 |
. . . . . . . . . . 11
⊢
1o ⊊ 2o |
24 | | ssnpss 4038 |
. . . . . . . . . . 11
⊢
(2o ⊆ 1o → ¬ 1o ⊊
2o) |
25 | 23, 24 | mt2 199 |
. . . . . . . . . 10
⊢ ¬
2o ⊆ 1o |
26 | | sseq2 3947 |
. . . . . . . . . 10
⊢ (𝑁 = 1o →
(2o ⊆ 𝑁
↔ 2o ⊆ 1o)) |
27 | 25, 26 | mtbiri 327 |
. . . . . . . . 9
⊢ (𝑁 = 1o → ¬
2o ⊆ 𝑁) |
28 | 27 | con2i 139 |
. . . . . . . 8
⊢
(2o ⊆ 𝑁 → ¬ 𝑁 = 1o) |
29 | 28 | intnanrd 490 |
. . . . . . 7
⊢
(2o ⊆ 𝑁 → ¬ (𝑁 = 1o ∧ 𝑋 ∈ 𝑈)) |
30 | 29 | iffalsed 4470 |
. . . . . 6
⊢
(2o ⊆ 𝑁 → if((𝑁 = 1o ∧ 𝑋 ∈ 𝑈), ∅, if(𝑋 ∈ (V × 𝑈), 〈∪ 𝑁, (1st ‘𝑋)〉, 〈𝑁, 𝑋〉)) = if(𝑋 ∈ (V × 𝑈), 〈∪ 𝑁, (1st ‘𝑋)〉, 〈𝑁, 𝑋〉)) |
31 | | iftrue 4465 |
. . . . . 6
⊢ (𝑋 ∈ (V × 𝑈) → if(𝑋 ∈ (V × 𝑈), 〈∪ 𝑁, (1st ‘𝑋)〉, 〈𝑁, 𝑋〉) = 〈∪
𝑁, (1st
‘𝑋)〉) |
32 | 30, 31 | sylan9eq 2798 |
. . . . 5
⊢
((2o ⊆ 𝑁 ∧ 𝑋 ∈ (V × 𝑈)) → if((𝑁 = 1o ∧ 𝑋 ∈ 𝑈), ∅, if(𝑋 ∈ (V × 𝑈), 〈∪ 𝑁, (1st ‘𝑋)〉, 〈𝑁, 𝑋〉)) = 〈∪ 𝑁,
(1st ‘𝑋)〉) |
33 | 15, 32 | sylan9eqr 2800 |
. . . 4
⊢
(((2o ⊆ 𝑁 ∧ 𝑋 ∈ (V × 𝑈)) ∧ (𝑛 = 𝑁 ∧ 𝑥 = 𝑋)) → if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = 〈∪
𝑁, (1st
‘𝑋)〉) |
34 | 33 | adantlll 715 |
. . 3
⊢ ((((𝑁 ∈ ω ∧
2o ⊆ 𝑁)
∧ 𝑋 ∈ (V ×
𝑈)) ∧ (𝑛 = 𝑁 ∧ 𝑥 = 𝑋)) → if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = 〈∪
𝑁, (1st
‘𝑋)〉) |
35 | | simpll 764 |
. . 3
⊢ (((𝑁 ∈ ω ∧
2o ⊆ 𝑁)
∧ 𝑋 ∈ (V ×
𝑈)) → 𝑁 ∈
ω) |
36 | | elex 3450 |
. . . 4
⊢ (𝑋 ∈ (V × 𝑈) → 𝑋 ∈ V) |
37 | 36 | adantl 482 |
. . 3
⊢ (((𝑁 ∈ ω ∧
2o ⊆ 𝑁)
∧ 𝑋 ∈ (V ×
𝑈)) → 𝑋 ∈ V) |
38 | | opex 5379 |
. . . 4
⊢
〈∪ 𝑁, (1st ‘𝑋)〉 ∈ V |
39 | 38 | a1i 11 |
. . 3
⊢ (((𝑁 ∈ ω ∧
2o ⊆ 𝑁)
∧ 𝑋 ∈ (V ×
𝑈)) → 〈∪ 𝑁,
(1st ‘𝑋)〉 ∈ V) |
40 | 2, 34, 35, 37, 39 | ovmpod 7425 |
. 2
⊢ (((𝑁 ∈ ω ∧
2o ⊆ 𝑁)
∧ 𝑋 ∈ (V ×
𝑈)) → (𝑁𝐹𝑋) = 〈∪ 𝑁, (1st ‘𝑋)〉) |
41 | | df-ov 7278 |
. 2
⊢ (𝑁𝐹𝑋) = (𝐹‘〈𝑁, 𝑋〉) |
42 | 40, 41 | eqtr3di 2793 |
1
⊢ (((𝑁 ∈ ω ∧
2o ⊆ 𝑁)
∧ 𝑋 ∈ (V ×
𝑈)) → 〈∪ 𝑁,
(1st ‘𝑋)〉 = (𝐹‘〈𝑁, 𝑋〉)) |