Proof of Theorem nofulllem4
Step | Hyp | Ref
| Expression |
1 | | nofulllem4.1 |
. 2
⊢ 𝑀 = ∩
{𝑎 ∈ On ∣
∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎)} |
2 | | unexg 6857 |
. . . . . . 7
⊢ ((𝐿 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝐿 ∪ 𝑅) ∈ V) |
3 | | nobndlem1 31091 |
. . . . . . . 8
⊢ ((𝐿 ∪ 𝑅) ∈ V → suc ∪ ( bday “ (𝐿 ∪ 𝑅)) ∈ On) |
4 | | sucelon 6909 |
. . . . . . . 8
⊢ (∪ ( bday “ (𝐿 ∪ 𝑅)) ∈ On ↔ suc ∪ ( bday “ (𝐿 ∪ 𝑅)) ∈ On) |
5 | 3, 4 | sylibr 223 |
. . . . . . 7
⊢ ((𝐿 ∪ 𝑅) ∈ V → ∪ ( bday “ (𝐿 ∪ 𝑅)) ∈ On) |
6 | 2, 5 | syl 17 |
. . . . . 6
⊢ ((𝐿 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ∪ ( bday “ (𝐿 ∪ 𝑅)) ∈ On) |
7 | 6 | ad2ant2l 778 |
. . . . 5
⊢ (((𝐿 ⊆
No ∧ 𝐿 ∈
𝑉) ∧ (𝑅 ⊆ No
∧ 𝑅 ∈ 𝑊)) → ∪ ( bday “ (𝐿 ∪ 𝑅)) ∈ On) |
8 | 7 | 3adant3 1074 |
. . . 4
⊢ (((𝐿 ⊆
No ∧ 𝐿 ∈
𝑉) ∧ (𝑅 ⊆ No
∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → ∪ ( bday “ (𝐿 ∪ 𝑅)) ∈ On) |
9 | | simprl 790 |
. . . . . . . . . . 11
⊢ (((𝐿 ⊆
No ∧ 𝐿 ∈
𝑉) ∧ (𝑅 ⊆ No
∧ 𝑅 ∈ 𝑊)) → 𝑅 ⊆ No
) |
10 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑅) → 𝑦 ∈ 𝑅) |
11 | | ssel2 3563 |
. . . . . . . . . . 11
⊢ ((𝑅 ⊆
No ∧ 𝑦 ∈
𝑅) → 𝑦 ∈
No ) |
12 | 9, 10, 11 | syl2an 493 |
. . . . . . . . . 10
⊢ ((((𝐿 ⊆
No ∧ 𝐿 ∈
𝑉) ∧ (𝑅 ⊆ No
∧ 𝑅 ∈ 𝑊)) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑅)) → 𝑦 ∈ No
) |
13 | | sltirr 31069 |
. . . . . . . . . 10
⊢ (𝑦 ∈
No → ¬ 𝑦
<s 𝑦) |
14 | | breq1 4586 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝑥 <s 𝑦 ↔ 𝑦 <s 𝑦)) |
15 | 14 | notbid 307 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (¬ 𝑥 <s 𝑦 ↔ ¬ 𝑦 <s 𝑦)) |
16 | 15 | biimprcd 239 |
. . . . . . . . . . 11
⊢ (¬
𝑦 <s 𝑦 → (𝑥 = 𝑦 → ¬ 𝑥 <s 𝑦)) |
17 | 16 | necon2ad 2797 |
. . . . . . . . . 10
⊢ (¬
𝑦 <s 𝑦 → (𝑥 <s 𝑦 → 𝑥 ≠ 𝑦)) |
18 | 12, 13, 17 | 3syl 18 |
. . . . . . . . 9
⊢ ((((𝐿 ⊆
No ∧ 𝐿 ∈
𝑉) ∧ (𝑅 ⊆ No
∧ 𝑅 ∈ 𝑊)) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑅)) → (𝑥 <s 𝑦 → 𝑥 ≠ 𝑦)) |
19 | 18 | impr 647 |
. . . . . . . 8
⊢ ((((𝐿 ⊆
No ∧ 𝐿 ∈
𝑉) ∧ (𝑅 ⊆ No
∧ 𝑅 ∈ 𝑊)) ∧ ((𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑅) ∧ 𝑥 <s 𝑦)) → 𝑥 ≠ 𝑦) |
20 | | simpll 786 |
. . . . . . . . 9
⊢ (((𝐿 ⊆
No ∧ 𝐿 ∈
𝑉) ∧ (𝑅 ⊆ No
∧ 𝑅 ∈ 𝑊)) → 𝐿 ⊆ No
) |
21 | | simpll 786 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑅) ∧ 𝑥 <s 𝑦) → 𝑥 ∈ 𝐿) |
22 | | ssun1 3738 |
. . . . . . . . . 10
⊢ 𝐿 ⊆ (𝐿 ∪ 𝑅) |
23 | | nofulllem3 31103 |
. . . . . . . . . 10
⊢ ((𝐿 ⊆
No ∧ 𝑥 ∈
𝐿 ∧ 𝐿 ⊆ (𝐿 ∪ 𝑅)) → (𝑥 ↾ ∪ ( bday “ (𝐿 ∪ 𝑅))) = 𝑥) |
24 | 22, 23 | mp3an3 1405 |
. . . . . . . . 9
⊢ ((𝐿 ⊆
No ∧ 𝑥 ∈
𝐿) → (𝑥 ↾ ∪ ( bday “ (𝐿 ∪ 𝑅))) = 𝑥) |
25 | 20, 21, 24 | syl2an 493 |
. . . . . . . 8
⊢ ((((𝐿 ⊆
No ∧ 𝐿 ∈
𝑉) ∧ (𝑅 ⊆ No
∧ 𝑅 ∈ 𝑊)) ∧ ((𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑅) ∧ 𝑥 <s 𝑦)) → (𝑥 ↾ ∪ ( bday “ (𝐿 ∪ 𝑅))) = 𝑥) |
26 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑅) ∧ 𝑥 <s 𝑦) → 𝑦 ∈ 𝑅) |
27 | | ssun2 3739 |
. . . . . . . . . 10
⊢ 𝑅 ⊆ (𝐿 ∪ 𝑅) |
28 | | nofulllem3 31103 |
. . . . . . . . . 10
⊢ ((𝑅 ⊆
No ∧ 𝑦 ∈
𝑅 ∧ 𝑅 ⊆ (𝐿 ∪ 𝑅)) → (𝑦 ↾ ∪ ( bday “ (𝐿 ∪ 𝑅))) = 𝑦) |
29 | 27, 28 | mp3an3 1405 |
. . . . . . . . 9
⊢ ((𝑅 ⊆
No ∧ 𝑦 ∈
𝑅) → (𝑦 ↾ ∪ ( bday “ (𝐿 ∪ 𝑅))) = 𝑦) |
30 | 9, 26, 29 | syl2an 493 |
. . . . . . . 8
⊢ ((((𝐿 ⊆
No ∧ 𝐿 ∈
𝑉) ∧ (𝑅 ⊆ No
∧ 𝑅 ∈ 𝑊)) ∧ ((𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑅) ∧ 𝑥 <s 𝑦)) → (𝑦 ↾ ∪ ( bday “ (𝐿 ∪ 𝑅))) = 𝑦) |
31 | 19, 25, 30 | 3netr4d 2859 |
. . . . . . 7
⊢ ((((𝐿 ⊆
No ∧ 𝐿 ∈
𝑉) ∧ (𝑅 ⊆ No
∧ 𝑅 ∈ 𝑊)) ∧ ((𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑅) ∧ 𝑥 <s 𝑦)) → (𝑥 ↾ ∪ ( bday “ (𝐿 ∪ 𝑅))) ≠ (𝑦 ↾ ∪ ( bday “ (𝐿 ∪ 𝑅)))) |
32 | 31 | expr 641 |
. . . . . 6
⊢ ((((𝐿 ⊆
No ∧ 𝐿 ∈
𝑉) ∧ (𝑅 ⊆ No
∧ 𝑅 ∈ 𝑊)) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑅)) → (𝑥 <s 𝑦 → (𝑥 ↾ ∪ ( bday “ (𝐿 ∪ 𝑅))) ≠ (𝑦 ↾ ∪ ( bday “ (𝐿 ∪ 𝑅))))) |
33 | 32 | ralimdvva 2947 |
. . . . 5
⊢ (((𝐿 ⊆
No ∧ 𝐿 ∈
𝑉) ∧ (𝑅 ⊆ No
∧ 𝑅 ∈ 𝑊)) → (∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦 → ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ ∪ ( bday “ (𝐿 ∪ 𝑅))) ≠ (𝑦 ↾ ∪ ( bday “ (𝐿 ∪ 𝑅))))) |
34 | 33 | 3impia 1253 |
. . . 4
⊢ (((𝐿 ⊆
No ∧ 𝐿 ∈
𝑉) ∧ (𝑅 ⊆ No
∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ ∪ ( bday “ (𝐿 ∪ 𝑅))) ≠ (𝑦 ↾ ∪ ( bday “ (𝐿 ∪ 𝑅)))) |
35 | | reseq2 5312 |
. . . . . . 7
⊢ (𝑎 = ∪
( bday “ (𝐿 ∪ 𝑅)) → (𝑥 ↾ 𝑎) = (𝑥 ↾ ∪ ( bday “ (𝐿 ∪ 𝑅)))) |
36 | | reseq2 5312 |
. . . . . . 7
⊢ (𝑎 = ∪
( bday “ (𝐿 ∪ 𝑅)) → (𝑦 ↾ 𝑎) = (𝑦 ↾ ∪ ( bday “ (𝐿 ∪ 𝑅)))) |
37 | 35, 36 | neeq12d 2843 |
. . . . . 6
⊢ (𝑎 = ∪
( bday “ (𝐿 ∪ 𝑅)) → ((𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎) ↔ (𝑥 ↾ ∪ ( bday “ (𝐿 ∪ 𝑅))) ≠ (𝑦 ↾ ∪ ( bday “ (𝐿 ∪ 𝑅))))) |
38 | 37 | 2ralbidv 2972 |
. . . . 5
⊢ (𝑎 = ∪
( bday “ (𝐿 ∪ 𝑅)) → (∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎) ↔ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ ∪ ( bday “ (𝐿 ∪ 𝑅))) ≠ (𝑦 ↾ ∪ ( bday “ (𝐿 ∪ 𝑅))))) |
39 | 38 | rspcev 3282 |
. . . 4
⊢ ((∪ ( bday “ (𝐿 ∪ 𝑅)) ∈ On ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ ∪ ( bday “ (𝐿 ∪ 𝑅))) ≠ (𝑦 ↾ ∪ ( bday “ (𝐿 ∪ 𝑅)))) → ∃𝑎 ∈ On ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎)) |
40 | 8, 34, 39 | syl2anc 691 |
. . 3
⊢ (((𝐿 ⊆
No ∧ 𝐿 ∈
𝑉) ∧ (𝑅 ⊆ No
∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → ∃𝑎 ∈ On ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎)) |
41 | | onintrab2 6894 |
. . 3
⊢
(∃𝑎 ∈ On
∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎) ↔ ∩ {𝑎 ∈ On ∣ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎)} ∈ On) |
42 | 40, 41 | sylib 207 |
. 2
⊢ (((𝐿 ⊆
No ∧ 𝐿 ∈
𝑉) ∧ (𝑅 ⊆ No
∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → ∩ {𝑎 ∈ On ∣ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎)} ∈ On) |
43 | 1, 42 | syl5eqel 2692 |
1
⊢ (((𝐿 ⊆
No ∧ 𝐿 ∈
𝑉) ∧ (𝑅 ⊆ No
∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → 𝑀 ∈ On) |