Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. 2
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((On × On) ×
On) ∧ 𝑦 ∈ ((On
× On) × On) ∧ ((((1st ‘(1st
‘𝑥)) E
(1st ‘(1st ‘𝑦)) ∨ (1st
‘(1st ‘𝑥)) = (1st ‘(1st
‘𝑦))) ∧
((2nd ‘(1st ‘𝑥)) E (2nd ‘(1st
‘𝑦)) ∨
(2nd ‘(1st ‘𝑥)) = (2nd ‘(1st
‘𝑦))) ∧
((2nd ‘𝑥)
E (2nd ‘𝑦)
∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((On × On) × On) ∧
𝑦 ∈ ((On × On)
× On) ∧ ((((1st ‘(1st ‘𝑥)) E (1st
‘(1st ‘𝑦)) ∨ (1st
‘(1st ‘𝑥)) = (1st ‘(1st
‘𝑦))) ∧
((2nd ‘(1st ‘𝑥)) E (2nd ‘(1st
‘𝑦)) ∨
(2nd ‘(1st ‘𝑥)) = (2nd ‘(1st
‘𝑦))) ∧
((2nd ‘𝑥)
E (2nd ‘𝑦)
∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))} |
2 | | onfr 6205 |
. 2
⊢ E Fr
On |
3 | | epweon 7510 |
. . 3
⊢ E We
On |
4 | | weso 5510 |
. . 3
⊢ ( E We On
→ E Or On) |
5 | | sopo 5456 |
. . 3
⊢ ( E Or On
→ E Po On) |
6 | 3, 4, 5 | mp2b 10 |
. 2
⊢ E Po
On |
7 | | epse 5502 |
. 2
⊢ E Se
On |
8 | | on3ind.1 |
. 2
⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜓)) |
9 | | on3ind.2 |
. 2
⊢ (𝑏 = 𝑒 → (𝜓 ↔ 𝜒)) |
10 | | on3ind.3 |
. 2
⊢ (𝑐 = 𝑓 → (𝜒 ↔ 𝜃)) |
11 | | on3ind.4 |
. 2
⊢ (𝑎 = 𝑑 → (𝜏 ↔ 𝜃)) |
12 | | on3ind.5 |
. 2
⊢ (𝑏 = 𝑒 → (𝜂 ↔ 𝜏)) |
13 | | on3ind.6 |
. 2
⊢ (𝑏 = 𝑒 → (𝜁 ↔ 𝜃)) |
14 | | on3ind.7 |
. 2
⊢ (𝑐 = 𝑓 → (𝜎 ↔ 𝜏)) |
15 | | on3ind.8 |
. 2
⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜌)) |
16 | | on3ind.9 |
. 2
⊢ (𝑏 = 𝑌 → (𝜌 ↔ 𝜇)) |
17 | | on3ind.10 |
. 2
⊢ (𝑐 = 𝑍 → (𝜇 ↔ 𝜆)) |
18 | | predon 7519 |
. . . . . . 7
⊢ (𝑎 ∈ On → Pred( E , On,
𝑎) = 𝑎) |
19 | 18 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) → Pred( E , On,
𝑎) = 𝑎) |
20 | | predon 7519 |
. . . . . . . 8
⊢ (𝑏 ∈ On → Pred( E , On,
𝑏) = 𝑏) |
21 | 20 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) → Pred( E , On,
𝑏) = 𝑏) |
22 | | predon 7519 |
. . . . . . . . 9
⊢ (𝑐 ∈ On → Pred( E , On,
𝑐) = 𝑐) |
23 | 22 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) → Pred( E , On,
𝑐) = 𝑐) |
24 | 23 | raleqdv 3315 |
. . . . . . 7
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑓 ∈ Pred ( E
, On, 𝑐)𝜃 ↔ ∀𝑓 ∈ 𝑐 𝜃)) |
25 | 21, 24 | raleqbidv 3303 |
. . . . . 6
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑒 ∈ Pred ( E
, On, 𝑏)∀𝑓 ∈ Pred ( E , On, 𝑐)𝜃 ↔ ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜃)) |
26 | 19, 25 | raleqbidv 3303 |
. . . . 5
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑑 ∈ Pred ( E
, On, 𝑎)∀𝑒 ∈ Pred ( E , On, 𝑏)∀𝑓 ∈ Pred ( E , On, 𝑐)𝜃 ↔ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜃)) |
27 | 21 | raleqdv 3315 |
. . . . . 6
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑒 ∈ Pred ( E
, On, 𝑏)𝜒 ↔ ∀𝑒 ∈ 𝑏 𝜒)) |
28 | 19, 27 | raleqbidv 3303 |
. . . . 5
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑑 ∈ Pred ( E
, On, 𝑎)∀𝑒 ∈ Pred ( E , On, 𝑏)𝜒 ↔ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ 𝑏 𝜒)) |
29 | 23 | raleqdv 3315 |
. . . . . 6
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑓 ∈ Pred ( E
, On, 𝑐)𝜁 ↔ ∀𝑓 ∈ 𝑐 𝜁)) |
30 | 19, 29 | raleqbidv 3303 |
. . . . 5
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑑 ∈ Pred ( E
, On, 𝑎)∀𝑓 ∈ Pred ( E , On, 𝑐)𝜁 ↔ ∀𝑑 ∈ 𝑎 ∀𝑓 ∈ 𝑐 𝜁)) |
31 | 26, 28, 30 | 3anbi123d 1437 |
. . . 4
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
((∀𝑑 ∈ Pred ( E
, On, 𝑎)∀𝑒 ∈ Pred ( E , On, 𝑏)∀𝑓 ∈ Pred ( E , On, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred ( E , On, 𝑎)∀𝑒 ∈ Pred ( E , On, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred ( E , On, 𝑎)∀𝑓 ∈ Pred ( E , On, 𝑐)𝜁) ↔ (∀𝑑 ∈ 𝑎 ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜃 ∧ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ 𝑏 𝜒 ∧ ∀𝑑 ∈ 𝑎 ∀𝑓 ∈ 𝑐 𝜁))) |
32 | 19 | raleqdv 3315 |
. . . . 5
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑑 ∈ Pred ( E
, On, 𝑎)𝜓 ↔ ∀𝑑 ∈ 𝑎 𝜓)) |
33 | 23 | raleqdv 3315 |
. . . . . 6
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑓 ∈ Pred ( E
, On, 𝑐)𝜏 ↔ ∀𝑓 ∈ 𝑐 𝜏)) |
34 | 21, 33 | raleqbidv 3303 |
. . . . 5
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑒 ∈ Pred ( E
, On, 𝑏)∀𝑓 ∈ Pred ( E , On, 𝑐)𝜏 ↔ ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜏)) |
35 | 21 | raleqdv 3315 |
. . . . 5
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑒 ∈ Pred ( E
, On, 𝑏)𝜎 ↔ ∀𝑒 ∈ 𝑏 𝜎)) |
36 | 32, 34, 35 | 3anbi123d 1437 |
. . . 4
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
((∀𝑑 ∈ Pred ( E
, On, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred ( E , On, 𝑏)∀𝑓 ∈ Pred ( E , On, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred ( E , On, 𝑏)𝜎) ↔ (∀𝑑 ∈ 𝑎 𝜓 ∧ ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜏 ∧ ∀𝑒 ∈ 𝑏 𝜎))) |
37 | 23 | raleqdv 3315 |
. . . 4
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑓 ∈ Pred ( E
, On, 𝑐)𝜂 ↔ ∀𝑓 ∈ 𝑐 𝜂)) |
38 | 31, 36, 37 | 3anbi123d 1437 |
. . 3
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(((∀𝑑 ∈ Pred (
E , On, 𝑎)∀𝑒 ∈ Pred ( E , On, 𝑏)∀𝑓 ∈ Pred ( E , On, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred ( E , On, 𝑎)∀𝑒 ∈ Pred ( E , On, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred ( E , On, 𝑎)∀𝑓 ∈ Pred ( E , On, 𝑐)𝜁) ∧ (∀𝑑 ∈ Pred ( E , On, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred ( E , On, 𝑏)∀𝑓 ∈ Pred ( E , On, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred ( E , On, 𝑏)𝜎) ∧ ∀𝑓 ∈ Pred ( E , On, 𝑐)𝜂) ↔ ((∀𝑑 ∈ 𝑎 ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜃 ∧ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ 𝑏 𝜒 ∧ ∀𝑑 ∈ 𝑎 ∀𝑓 ∈ 𝑐 𝜁) ∧ (∀𝑑 ∈ 𝑎 𝜓 ∧ ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜏 ∧ ∀𝑒 ∈ 𝑏 𝜎) ∧ ∀𝑓 ∈ 𝑐 𝜂))) |
39 | | on3ind.i |
. . 3
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(((∀𝑑 ∈ 𝑎 ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜃 ∧ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ 𝑏 𝜒 ∧ ∀𝑑 ∈ 𝑎 ∀𝑓 ∈ 𝑐 𝜁) ∧ (∀𝑑 ∈ 𝑎 𝜓 ∧ ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜏 ∧ ∀𝑒 ∈ 𝑏 𝜎) ∧ ∀𝑓 ∈ 𝑐 𝜂) → 𝜑)) |
40 | 38, 39 | sylbid 243 |
. 2
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(((∀𝑑 ∈ Pred (
E , On, 𝑎)∀𝑒 ∈ Pred ( E , On, 𝑏)∀𝑓 ∈ Pred ( E , On, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred ( E , On, 𝑎)∀𝑒 ∈ Pred ( E , On, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred ( E , On, 𝑎)∀𝑓 ∈ Pred ( E , On, 𝑐)𝜁) ∧ (∀𝑑 ∈ Pred ( E , On, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred ( E , On, 𝑏)∀𝑓 ∈ Pred ( E , On, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred ( E , On, 𝑏)𝜎) ∧ ∀𝑓 ∈ Pred ( E , On, 𝑐)𝜂) → 𝜑)) |
41 | 1, 2, 6, 7, 2, 6, 7, 2, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 40 | xpord3ind 33403 |
1
⊢ ((𝑋 ∈ On ∧ 𝑌 ∈ On ∧ 𝑍 ∈ On) → 𝜆) |