Proof of Theorem tfsconcatb0
Step | Hyp | Ref
| Expression |
1 | | fnrel 6641 |
. . . . . . 7
⊢ (𝐵 Fn 𝐷 → Rel 𝐵) |
2 | | reldm0 5917 |
. . . . . . 7
⊢ (Rel
𝐵 → (𝐵 = ∅ ↔ dom 𝐵 = ∅)) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢ (𝐵 Fn 𝐷 → (𝐵 = ∅ ↔ dom 𝐵 = ∅)) |
4 | | fndm 6642 |
. . . . . . 7
⊢ (𝐵 Fn 𝐷 → dom 𝐵 = 𝐷) |
5 | 4 | eqeq1d 2726 |
. . . . . 6
⊢ (𝐵 Fn 𝐷 → (dom 𝐵 = ∅ ↔ 𝐷 = ∅)) |
6 | 3, 5 | bitrd 279 |
. . . . 5
⊢ (𝐵 Fn 𝐷 → (𝐵 = ∅ ↔ 𝐷 = ∅)) |
7 | 6 | ad2antlr 724 |
. . . 4
⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (𝐵 = ∅ ↔ 𝐷 = ∅)) |
8 | | rex0 4349 |
. . . . . . . . . . 11
⊢ ¬
∃𝑧 ∈ ∅
(𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)) |
9 | | rexeq 3313 |
. . . . . . . . . . . 12
⊢ (𝐷 = ∅ → (∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)) ↔ ∃𝑧 ∈ ∅ (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))) |
10 | 9 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 𝐷 = ∅) → (∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)) ↔ ∃𝑧 ∈ ∅ (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))) |
11 | 8, 10 | mtbiri 327 |
. . . . . . . . . 10
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 𝐷 = ∅) → ¬ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧))) |
12 | 11 | intnand 488 |
. . . . . . . . 9
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 𝐷 = ∅) → ¬ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))) |
13 | 12 | alrimivv 1923 |
. . . . . . . 8
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 𝐷 = ∅) → ∀𝑥∀𝑦 ¬ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))) |
14 | | opab0 5544 |
. . . . . . . 8
⊢
({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))} = ∅ ↔ ∀𝑥∀𝑦 ¬ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))) |
15 | 13, 14 | sylibr 233 |
. . . . . . 7
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 𝐷 = ∅) → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))} = ∅) |
16 | | 0ss 4388 |
. . . . . . 7
⊢ ∅
⊆ 𝐴 |
17 | 15, 16 | eqsstrdi 4028 |
. . . . . 6
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 𝐷 = ∅) → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))} ⊆ 𝐴) |
18 | 17 | ex 412 |
. . . . 5
⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (𝐷 = ∅ → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))} ⊆ 𝐴)) |
19 | | df-1o 8461 |
. . . . . . . . . 10
⊢
1o = suc ∅ |
20 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ On ∧ ¬ 𝐷 = ∅) → 𝐷 ∈ On) |
21 | | on0eln0 6410 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∈ On → (∅
∈ 𝐷 ↔ 𝐷 ≠ ∅)) |
22 | | df-ne 2933 |
. . . . . . . . . . . . 13
⊢ (𝐷 ≠ ∅ ↔ ¬ 𝐷 = ∅) |
23 | 21, 22 | bitrdi 287 |
. . . . . . . . . . . 12
⊢ (𝐷 ∈ On → (∅
∈ 𝐷 ↔ ¬ 𝐷 = ∅)) |
24 | 23 | biimpar 477 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ On ∧ ¬ 𝐷 = ∅) → ∅
∈ 𝐷) |
25 | | onsucss 42471 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ On → (∅
∈ 𝐷 → suc ∅
⊆ 𝐷)) |
26 | 20, 24, 25 | sylc 65 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ On ∧ ¬ 𝐷 = ∅) → suc ∅
⊆ 𝐷) |
27 | 19, 26 | eqsstrid 4022 |
. . . . . . . . 9
⊢ ((𝐷 ∈ On ∧ ¬ 𝐷 = ∅) → 1o
⊆ 𝐷) |
28 | 27 | ex 412 |
. . . . . . . 8
⊢ (𝐷 ∈ On → (¬ 𝐷 = ∅ → 1o
⊆ 𝐷)) |
29 | 28 | adantl 481 |
. . . . . . 7
⊢ ((𝐶 ∈ On ∧ 𝐷 ∈ On) → (¬ 𝐷 = ∅ → 1o
⊆ 𝐷)) |
30 | 29 | adantl 481 |
. . . . . 6
⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (¬ 𝐷 = ∅ → 1o ⊆
𝐷)) |
31 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 1o ⊆
𝐷) → 1o
⊆ 𝐷) |
32 | | 0lt1o 8499 |
. . . . . . . . . . . . . 14
⊢ ∅
∈ 1o |
33 | 32 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 1o ⊆
𝐷) → ∅ ∈
1o) |
34 | 31, 33 | sseldd 3975 |
. . . . . . . . . . . 12
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 1o ⊆
𝐷) → ∅ ∈
𝐷) |
35 | | oaord1 8546 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ On ∧ 𝐷 ∈ On) → (∅
∈ 𝐷 ↔ 𝐶 ∈ (𝐶 +o 𝐷))) |
36 | 35 | ad2antlr 724 |
. . . . . . . . . . . 12
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 1o ⊆
𝐷) → (∅ ∈
𝐷 ↔ 𝐶 ∈ (𝐶 +o 𝐷))) |
37 | 34, 36 | mpbid 231 |
. . . . . . . . . . 11
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 1o ⊆
𝐷) → 𝐶 ∈ (𝐶 +o 𝐷)) |
38 | | ssidd 3997 |
. . . . . . . . . . 11
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 1o ⊆
𝐷) → 𝐶 ⊆ 𝐶) |
39 | | oacl 8530 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ On ∧ 𝐷 ∈ On) → (𝐶 +o 𝐷) ∈ On) |
40 | | eloni 6364 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 +o 𝐷) ∈ On → Ord (𝐶 +o 𝐷)) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ On ∧ 𝐷 ∈ On) → Ord (𝐶 +o 𝐷)) |
42 | | eloni 6364 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∈ On → Ord 𝐶) |
43 | 42 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ On ∧ 𝐷 ∈ On) → Ord 𝐶) |
44 | 41, 43 | jca 511 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ On ∧ 𝐷 ∈ On) → (Ord (𝐶 +o 𝐷) ∧ Ord 𝐶)) |
45 | 44 | ad2antlr 724 |
. . . . . . . . . . . 12
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 1o ⊆
𝐷) → (Ord (𝐶 +o 𝐷) ∧ Ord 𝐶)) |
46 | | ordeldif 42463 |
. . . . . . . . . . . 12
⊢ ((Ord
(𝐶 +o 𝐷) ∧ Ord 𝐶) → (𝐶 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ↔ (𝐶 ∈ (𝐶 +o 𝐷) ∧ 𝐶 ⊆ 𝐶))) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 1o ⊆
𝐷) → (𝐶 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ↔ (𝐶 ∈ (𝐶 +o 𝐷) ∧ 𝐶 ⊆ 𝐶))) |
48 | 37, 38, 47 | mpbir2and 710 |
. . . . . . . . . 10
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 1o ⊆
𝐷) → 𝐶 ∈ ((𝐶 +o 𝐷) ∖ 𝐶)) |
49 | | simpl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ On ∧ 𝐷 ∈ On) → 𝐶 ∈ On) |
50 | 49 | ad2antlr 724 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 1o ⊆
𝐷) → 𝐶 ∈ On) |
51 | | oa0 8511 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∈ On → (𝐶 +o ∅) = 𝐶) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 1o ⊆
𝐷) → (𝐶 +o ∅) = 𝐶) |
53 | 52 | eqcomd 2730 |
. . . . . . . . . . . 12
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 1o ⊆
𝐷) → 𝐶 = (𝐶 +o ∅)) |
54 | | eqidd 2725 |
. . . . . . . . . . . 12
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 1o ⊆
𝐷) → (𝐵‘∅) = (𝐵‘∅)) |
55 | 53, 54 | jca 511 |
. . . . . . . . . . 11
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 1o ⊆
𝐷) → (𝐶 = (𝐶 +o ∅) ∧ (𝐵‘∅) = (𝐵‘∅))) |
56 | | oveq2 7409 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = ∅ → (𝐶 +o 𝑧) = (𝐶 +o ∅)) |
57 | 56 | eqeq2d 2735 |
. . . . . . . . . . . . 13
⊢ (𝑧 = ∅ → (𝐶 = (𝐶 +o 𝑧) ↔ 𝐶 = (𝐶 +o ∅))) |
58 | | fveq2 6881 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = ∅ → (𝐵‘𝑧) = (𝐵‘∅)) |
59 | 58 | eqeq2d 2735 |
. . . . . . . . . . . . 13
⊢ (𝑧 = ∅ → ((𝐵‘∅) = (𝐵‘𝑧) ↔ (𝐵‘∅) = (𝐵‘∅))) |
60 | 57, 59 | anbi12d 630 |
. . . . . . . . . . . 12
⊢ (𝑧 = ∅ → ((𝐶 = (𝐶 +o 𝑧) ∧ (𝐵‘∅) = (𝐵‘𝑧)) ↔ (𝐶 = (𝐶 +o ∅) ∧ (𝐵‘∅) = (𝐵‘∅)))) |
61 | 60 | rspcev 3604 |
. . . . . . . . . . 11
⊢ ((∅
∈ 𝐷 ∧ (𝐶 = (𝐶 +o ∅) ∧ (𝐵‘∅) = (𝐵‘∅))) →
∃𝑧 ∈ 𝐷 (𝐶 = (𝐶 +o 𝑧) ∧ (𝐵‘∅) = (𝐵‘𝑧))) |
62 | 34, 55, 61 | syl2anc 583 |
. . . . . . . . . 10
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 1o ⊆
𝐷) → ∃𝑧 ∈ 𝐷 (𝐶 = (𝐶 +o 𝑧) ∧ (𝐵‘∅) = (𝐵‘𝑧))) |
63 | | fvexd 6896 |
. . . . . . . . . . 11
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 1o ⊆
𝐷) → (𝐵‘∅) ∈
V) |
64 | | eleq1 2813 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐶 → (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ↔ 𝐶 ∈ ((𝐶 +o 𝐷) ∖ 𝐶))) |
65 | 64 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝐶 ∧ 𝑦 = (𝐵‘∅)) → (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ↔ 𝐶 ∈ ((𝐶 +o 𝐷) ∖ 𝐶))) |
66 | | eqeq1 2728 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐶 → (𝑥 = (𝐶 +o 𝑧) ↔ 𝐶 = (𝐶 +o 𝑧))) |
67 | | eqeq1 2728 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝐵‘∅) → (𝑦 = (𝐵‘𝑧) ↔ (𝐵‘∅) = (𝐵‘𝑧))) |
68 | 66, 67 | bi2anan9 636 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 𝐶 ∧ 𝑦 = (𝐵‘∅)) → ((𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)) ↔ (𝐶 = (𝐶 +o 𝑧) ∧ (𝐵‘∅) = (𝐵‘𝑧)))) |
69 | 68 | rexbidv 3170 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝐶 ∧ 𝑦 = (𝐵‘∅)) → (∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)) ↔ ∃𝑧 ∈ 𝐷 (𝐶 = (𝐶 +o 𝑧) ∧ (𝐵‘∅) = (𝐵‘𝑧)))) |
70 | 65, 69 | anbi12d 630 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝐶 ∧ 𝑦 = (𝐵‘∅)) → ((𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧))) ↔ (𝐶 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝐶 = (𝐶 +o 𝑧) ∧ (𝐵‘∅) = (𝐵‘𝑧))))) |
71 | 70 | opelopabga 5523 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ On ∧ (𝐵‘∅) ∈ V) →
(〈𝐶, (𝐵‘∅)〉 ∈
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))} ↔ (𝐶 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝐶 = (𝐶 +o 𝑧) ∧ (𝐵‘∅) = (𝐵‘𝑧))))) |
72 | 50, 63, 71 | syl2anc 583 |
. . . . . . . . . 10
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 1o ⊆
𝐷) → (〈𝐶, (𝐵‘∅)〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))} ↔ (𝐶 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝐶 = (𝐶 +o 𝑧) ∧ (𝐵‘∅) = (𝐵‘𝑧))))) |
73 | 48, 62, 72 | mpbir2and 710 |
. . . . . . . . 9
⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 1o ⊆
𝐷) → 〈𝐶, (𝐵‘∅)〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))}) |
74 | 73 | ex 412 |
. . . . . . . 8
⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (1o ⊆
𝐷 → 〈𝐶, (𝐵‘∅)〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))})) |
75 | | ordirr 6372 |
. . . . . . . . . . . . 13
⊢ (Ord
𝐶 → ¬ 𝐶 ∈ 𝐶) |
76 | 42, 75 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ On → ¬ 𝐶 ∈ 𝐶) |
77 | 76 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ On ∧ 𝐷 ∈ On) → ¬ 𝐶 ∈ 𝐶) |
78 | 77 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → ¬ 𝐶 ∈ 𝐶) |
79 | | fndm 6642 |
. . . . . . . . . . . 12
⊢ (𝐴 Fn 𝐶 → dom 𝐴 = 𝐶) |
80 | 79 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) → dom 𝐴 = 𝐶) |
81 | 80 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → dom 𝐴 = 𝐶) |
82 | 78, 81 | neleqtrrd 2848 |
. . . . . . . . 9
⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → ¬ 𝐶 ∈ dom 𝐴) |
83 | 49 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → 𝐶 ∈ On) |
84 | | fvexd 6896 |
. . . . . . . . . 10
⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (𝐵‘∅) ∈ V) |
85 | 83, 84 | opeldmd 5896 |
. . . . . . . . 9
⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (〈𝐶, (𝐵‘∅)〉 ∈ 𝐴 → 𝐶 ∈ dom 𝐴)) |
86 | 82, 85 | mtod 197 |
. . . . . . . 8
⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → ¬ 〈𝐶, (𝐵‘∅)〉 ∈ 𝐴) |
87 | 74, 86 | jctird 526 |
. . . . . . 7
⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (1o ⊆
𝐷 → (〈𝐶, (𝐵‘∅)〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))} ∧ ¬ 〈𝐶, (𝐵‘∅)〉 ∈ 𝐴))) |
88 | | nelss 4039 |
. . . . . . 7
⊢
((〈𝐶, (𝐵‘∅)〉 ∈
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))} ∧ ¬ 〈𝐶, (𝐵‘∅)〉 ∈ 𝐴) → ¬ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))} ⊆ 𝐴) |
89 | 87, 88 | syl6 35 |
. . . . . 6
⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (1o ⊆
𝐷 → ¬ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))} ⊆ 𝐴)) |
90 | 30, 89 | syld 47 |
. . . . 5
⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (¬ 𝐷 = ∅ → ¬ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))} ⊆ 𝐴)) |
91 | 18, 90 | impcon4bid 226 |
. . . 4
⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (𝐷 = ∅ ↔ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))} ⊆ 𝐴)) |
92 | 7, 91 | bitrd 279 |
. . 3
⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (𝐵 = ∅ ↔ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))} ⊆ 𝐴)) |
93 | | ssequn2 4175 |
. . 3
⊢
({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))} ⊆ 𝐴 ↔ (𝐴 ∪ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))}) = 𝐴) |
94 | 92, 93 | bitrdi 287 |
. 2
⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (𝐵 = ∅ ↔ (𝐴 ∪ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))}) = 𝐴)) |
95 | | tfsconcat.op |
. . . 4
⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))})) |
96 | 95 | tfsconcatun 42542 |
. . 3
⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (𝐴 + 𝐵) = (𝐴 ∪ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))})) |
97 | 96 | eqeq1d 2726 |
. 2
⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → ((𝐴 + 𝐵) = 𝐴 ↔ (𝐴 ∪ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))}) = 𝐴)) |
98 | 94, 97 | bitr4d 282 |
1
⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (𝐵 = ∅ ↔ (𝐴 + 𝐵) = 𝐴)) |