Proof of Theorem 2reu3
Step | Hyp | Ref
| Expression |
1 | | orcom 869 |
. . . . . . 7
⊢
((∃*𝑥 ∈
𝐴 𝜑 ∨ ∃*𝑦 ∈ 𝐵 𝜑) ↔ (∃*𝑦 ∈ 𝐵 𝜑 ∨ ∃*𝑥 ∈ 𝐴 𝜑)) |
2 | 1 | ralbii 3080 |
. . . . . 6
⊢
(∀𝑦 ∈
𝐵 (∃*𝑥 ∈ 𝐴 𝜑 ∨ ∃*𝑦 ∈ 𝐵 𝜑) ↔ ∀𝑦 ∈ 𝐵 (∃*𝑦 ∈ 𝐵 𝜑 ∨ ∃*𝑥 ∈ 𝐴 𝜑)) |
3 | | nfrmo1 3274 |
. . . . . . 7
⊢
Ⅎ𝑦∃*𝑦 ∈ 𝐵 𝜑 |
4 | 3 | r19.32 44142 |
. . . . . 6
⊢
(∀𝑦 ∈
𝐵 (∃*𝑦 ∈ 𝐵 𝜑 ∨ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃*𝑦 ∈ 𝐵 𝜑 ∨ ∀𝑦 ∈ 𝐵 ∃*𝑥 ∈ 𝐴 𝜑)) |
5 | 2, 4 | bitri 278 |
. . . . 5
⊢
(∀𝑦 ∈
𝐵 (∃*𝑥 ∈ 𝐴 𝜑 ∨ ∃*𝑦 ∈ 𝐵 𝜑) ↔ (∃*𝑦 ∈ 𝐵 𝜑 ∨ ∀𝑦 ∈ 𝐵 ∃*𝑥 ∈ 𝐴 𝜑)) |
6 | | orcom 869 |
. . . . 5
⊢
((∃*𝑦 ∈
𝐵 𝜑 ∨ ∀𝑦 ∈ 𝐵 ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∀𝑦 ∈ 𝐵 ∃*𝑥 ∈ 𝐴 𝜑 ∨ ∃*𝑦 ∈ 𝐵 𝜑)) |
7 | 5, 6 | bitri 278 |
. . . 4
⊢
(∀𝑦 ∈
𝐵 (∃*𝑥 ∈ 𝐴 𝜑 ∨ ∃*𝑦 ∈ 𝐵 𝜑) ↔ (∀𝑦 ∈ 𝐵 ∃*𝑥 ∈ 𝐴 𝜑 ∨ ∃*𝑦 ∈ 𝐵 𝜑)) |
8 | 7 | ralbii 3080 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 (∃*𝑥 ∈ 𝐴 𝜑 ∨ ∃*𝑦 ∈ 𝐵 𝜑) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ∃*𝑥 ∈ 𝐴 𝜑 ∨ ∃*𝑦 ∈ 𝐵 𝜑)) |
9 | | nfcv 2899 |
. . . . 5
⊢
Ⅎ𝑥𝐵 |
10 | | nfrmo1 3274 |
. . . . 5
⊢
Ⅎ𝑥∃*𝑥 ∈ 𝐴 𝜑 |
11 | 9, 10 | nfralw 3138 |
. . . 4
⊢
Ⅎ𝑥∀𝑦 ∈ 𝐵 ∃*𝑥 ∈ 𝐴 𝜑 |
12 | 11 | r19.32 44142 |
. . 3
⊢
(∀𝑥 ∈
𝐴 (∀𝑦 ∈ 𝐵 ∃*𝑥 ∈ 𝐴 𝜑 ∨ ∃*𝑦 ∈ 𝐵 𝜑) ↔ (∀𝑦 ∈ 𝐵 ∃*𝑥 ∈ 𝐴 𝜑 ∨ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝜑)) |
13 | 8, 12 | bitri 278 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 (∃*𝑥 ∈ 𝐴 𝜑 ∨ ∃*𝑦 ∈ 𝐵 𝜑) ↔ (∀𝑦 ∈ 𝐵 ∃*𝑥 ∈ 𝐴 𝜑 ∨ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝜑)) |
14 | | 2reu1 3788 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝐵 ∃*𝑥 ∈ 𝐴 𝜑 → (∃!𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑))) |
15 | 14 | biimpd 232 |
. . . . . 6
⊢
(∀𝑦 ∈
𝐵 ∃*𝑥 ∈ 𝐴 𝜑 → (∃!𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝜑 → (∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑))) |
16 | | ancom 464 |
. . . . . 6
⊢
((∃!𝑦 ∈
𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)) |
17 | 15, 16 | syl6ib 254 |
. . . . 5
⊢
(∀𝑦 ∈
𝐵 ∃*𝑥 ∈ 𝐴 𝜑 → (∃!𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝜑 → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))) |
18 | 17 | adantld 494 |
. . . 4
⊢
(∀𝑦 ∈
𝐵 ∃*𝑥 ∈ 𝐴 𝜑 → ((∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝜑) → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))) |
19 | | 2reu1 3788 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 ∃*𝑦 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))) |
20 | 19 | biimpd 232 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∃*𝑦 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))) |
21 | 20 | adantrd 495 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∃*𝑦 ∈ 𝐵 𝜑 → ((∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝜑) → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))) |
22 | 18, 21 | jaoi 856 |
. . 3
⊢
((∀𝑦 ∈
𝐵 ∃*𝑥 ∈ 𝐴 𝜑 ∨ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝜑) → ((∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝜑) → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))) |
23 | | 2rexreu 3661 |
. . . 4
⊢
((∃!𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) → ∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑) |
24 | | 2rexreu 3661 |
. . . . 5
⊢
((∃!𝑦 ∈
𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃!𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝜑) |
25 | 24 | ancoms 462 |
. . . 4
⊢
((∃!𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) → ∃!𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝜑) |
26 | 23, 25 | jca 515 |
. . 3
⊢
((∃!𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) → (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝜑)) |
27 | 22, 26 | impbid1 228 |
. 2
⊢
((∀𝑦 ∈
𝐵 ∃*𝑥 ∈ 𝐴 𝜑 ∨ ∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝜑) → ((∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝜑) ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))) |
28 | 13, 27 | sylbi 220 |
1
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 (∃*𝑥 ∈ 𝐴 𝜑 ∨ ∃*𝑦 ∈ 𝐵 𝜑) → ((∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝜑) ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))) |