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 2741 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (𝑛 = 1o ↔ 𝑁 = 1o)) |
| 4 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑥 ∈ 𝑈 ↔ 𝑋 ∈ 𝑈)) |
| 5 | 3, 4 | bi2anan9 638 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → ((𝑛 = 1o ∧ 𝑥 ∈ 𝑈) ↔ (𝑁 = 1o ∧ 𝑋 ∈ 𝑈))) |
| 6 | | eleq1 2829 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑥 ∈ (V × 𝑈) ↔ 𝑋 ∈ (V × 𝑈))) |
| 7 | 6 | adantl 481 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → (𝑥 ∈ (V × 𝑈) ↔ 𝑋 ∈ (V × 𝑈))) |
| 8 | | unieq 4918 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → ∪ 𝑛 = ∪
𝑁) |
| 9 | 8 | adantr 480 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → ∪ 𝑛 = ∪
𝑁) |
| 10 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (1st ‘𝑥) = (1st ‘𝑋)) |
| 11 | 10 | adantl 481 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → (1st ‘𝑥) = (1st ‘𝑋)) |
| 12 | 9, 11 | opeq12d 4881 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → 〈∪
𝑛, (1st
‘𝑥)〉 =
〈∪ 𝑁, (1st ‘𝑋)〉) |
| 13 | | opeq12 4875 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → 〈𝑛, 𝑥〉 = 〈𝑁, 𝑋〉) |
| 14 | 7, 12, 13 | ifbieq12d 4554 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = if(𝑋 ∈ (V × 𝑈), 〈∪ 𝑁, (1st ‘𝑋)〉, 〈𝑁, 𝑋〉)) |
| 15 | 5, 14 | ifbieq2d 4552 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑥 = 𝑋) → if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = if((𝑁 = 1o ∧ 𝑋 ∈ 𝑈), ∅, if(𝑋 ∈ (V × 𝑈), 〈∪ 𝑁, (1st ‘𝑋)〉, 〈𝑁, 𝑋〉))) |
| 16 | | sssucid 6464 |
. . . . . . . . . . . . 13
⊢
1o ⊆ suc 1o |
| 17 | | df-2o 8507 |
. . . . . . . . . . . . 13
⊢
2o = suc 1o |
| 18 | 16, 17 | sseqtrri 4033 |
. . . . . . . . . . . 12
⊢
1o ⊆ 2o |
| 19 | | 1on 8518 |
. . . . . . . . . . . . . 14
⊢
1o ∈ On |
| 20 | 17, 19 | sucneqoni 37367 |
. . . . . . . . . . . . 13
⊢
2o ≠ 1o |
| 21 | 20 | necomi 2995 |
. . . . . . . . . . . 12
⊢
1o ≠ 2o |
| 22 | | df-pss 3971 |
. . . . . . . . . . . 12
⊢
(1o ⊊ 2o ↔ (1o ⊆
2o ∧ 1o ≠ 2o)) |
| 23 | 18, 21, 22 | mpbir2an 711 |
. . . . . . . . . . 11
⊢
1o ⊊ 2o |
| 24 | | ssnpss 4106 |
. . . . . . . . . . 11
⊢
(2o ⊆ 1o → ¬ 1o ⊊
2o) |
| 25 | 23, 24 | mt2 200 |
. . . . . . . . . 10
⊢ ¬
2o ⊆ 1o |
| 26 | | sseq2 4010 |
. . . . . . . . . 10
⊢ (𝑁 = 1o →
(2o ⊆ 𝑁
↔ 2o ⊆ 1o)) |
| 27 | 25, 26 | mtbiri 327 |
. . . . . . . . 9
⊢ (𝑁 = 1o → ¬
2o ⊆ 𝑁) |
| 28 | 27 | con2i 139 |
. . . . . . . 8
⊢
(2o ⊆ 𝑁 → ¬ 𝑁 = 1o) |
| 29 | 28 | intnanrd 489 |
. . . . . . 7
⊢
(2o ⊆ 𝑁 → ¬ (𝑁 = 1o ∧ 𝑋 ∈ 𝑈)) |
| 30 | 29 | iffalsed 4536 |
. . . . . 6
⊢
(2o ⊆ 𝑁 → if((𝑁 = 1o ∧ 𝑋 ∈ 𝑈), ∅, if(𝑋 ∈ (V × 𝑈), 〈∪ 𝑁, (1st ‘𝑋)〉, 〈𝑁, 𝑋〉)) = if(𝑋 ∈ (V × 𝑈), 〈∪ 𝑁, (1st ‘𝑋)〉, 〈𝑁, 𝑋〉)) |
| 31 | | iftrue 4531 |
. . . . . 6
⊢ (𝑋 ∈ (V × 𝑈) → if(𝑋 ∈ (V × 𝑈), 〈∪ 𝑁, (1st ‘𝑋)〉, 〈𝑁, 𝑋〉) = 〈∪
𝑁, (1st
‘𝑋)〉) |
| 32 | 30, 31 | sylan9eq 2797 |
. . . . 5
⊢
((2o ⊆ 𝑁 ∧ 𝑋 ∈ (V × 𝑈)) → if((𝑁 = 1o ∧ 𝑋 ∈ 𝑈), ∅, if(𝑋 ∈ (V × 𝑈), 〈∪ 𝑁, (1st ‘𝑋)〉, 〈𝑁, 𝑋〉)) = 〈∪ 𝑁,
(1st ‘𝑋)〉) |
| 33 | 15, 32 | sylan9eqr 2799 |
. . . 4
⊢
(((2o ⊆ 𝑁 ∧ 𝑋 ∈ (V × 𝑈)) ∧ (𝑛 = 𝑁 ∧ 𝑥 = 𝑋)) → if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = 〈∪
𝑁, (1st
‘𝑋)〉) |
| 34 | 33 | adantlll 718 |
. . 3
⊢ ((((𝑁 ∈ ω ∧
2o ⊆ 𝑁)
∧ 𝑋 ∈ (V ×
𝑈)) ∧ (𝑛 = 𝑁 ∧ 𝑥 = 𝑋)) → if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = 〈∪
𝑁, (1st
‘𝑋)〉) |
| 35 | | simpll 767 |
. . 3
⊢ (((𝑁 ∈ ω ∧
2o ⊆ 𝑁)
∧ 𝑋 ∈ (V ×
𝑈)) → 𝑁 ∈
ω) |
| 36 | | elex 3501 |
. . . 4
⊢ (𝑋 ∈ (V × 𝑈) → 𝑋 ∈ V) |
| 37 | 36 | adantl 481 |
. . 3
⊢ (((𝑁 ∈ ω ∧
2o ⊆ 𝑁)
∧ 𝑋 ∈ (V ×
𝑈)) → 𝑋 ∈ V) |
| 38 | | opex 5469 |
. . . 4
⊢
〈∪ 𝑁, (1st ‘𝑋)〉 ∈ V |
| 39 | 38 | a1i 11 |
. . 3
⊢ (((𝑁 ∈ ω ∧
2o ⊆ 𝑁)
∧ 𝑋 ∈ (V ×
𝑈)) → 〈∪ 𝑁,
(1st ‘𝑋)〉 ∈ V) |
| 40 | 2, 34, 35, 37, 39 | ovmpod 7585 |
. 2
⊢ (((𝑁 ∈ ω ∧
2o ⊆ 𝑁)
∧ 𝑋 ∈ (V ×
𝑈)) → (𝑁𝐹𝑋) = 〈∪ 𝑁, (1st ‘𝑋)〉) |
| 41 | | df-ov 7434 |
. 2
⊢ (𝑁𝐹𝑋) = (𝐹‘〈𝑁, 𝑋〉) |
| 42 | 40, 41 | eqtr3di 2792 |
1
⊢ (((𝑁 ∈ ω ∧
2o ⊆ 𝑁)
∧ 𝑋 ∈ (V ×
𝑈)) → 〈∪ 𝑁,
(1st ‘𝑋)〉 = (𝐹‘〈𝑁, 𝑋〉)) |