Proof of Theorem on3ind
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | onfr 6422 | . 2
⊢  E Fr
On | 
| 2 |  | epweon 7796 | . . 3
⊢  E We
On | 
| 3 |  | weso 5675 | . . 3
⊢ ( E We On
→ E Or On) | 
| 4 |  | sopo 5610 | . . 3
⊢ ( E Or On
→ E Po On) | 
| 5 | 2, 3, 4 | mp2b 10 | . 2
⊢  E Po
On | 
| 6 |  | epse 5666 | . 2
⊢  E Se
On | 
| 7 |  | on3ind.1 | . 2
⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜓)) | 
| 8 |  | on3ind.2 | . 2
⊢ (𝑏 = 𝑒 → (𝜓 ↔ 𝜒)) | 
| 9 |  | on3ind.3 | . 2
⊢ (𝑐 = 𝑓 → (𝜒 ↔ 𝜃)) | 
| 10 |  | on3ind.4 | . 2
⊢ (𝑎 = 𝑑 → (𝜏 ↔ 𝜃)) | 
| 11 |  | on3ind.5 | . 2
⊢ (𝑏 = 𝑒 → (𝜂 ↔ 𝜏)) | 
| 12 |  | on3ind.6 | . 2
⊢ (𝑏 = 𝑒 → (𝜁 ↔ 𝜃)) | 
| 13 |  | on3ind.7 | . 2
⊢ (𝑐 = 𝑓 → (𝜎 ↔ 𝜏)) | 
| 14 |  | on3ind.8 | . 2
⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜌)) | 
| 15 |  | on3ind.9 | . 2
⊢ (𝑏 = 𝑌 → (𝜌 ↔ 𝜇)) | 
| 16 |  | on3ind.10 | . 2
⊢ (𝑐 = 𝑍 → (𝜇 ↔ 𝜆)) | 
| 17 |  | predon 7807 | . . . . . . 7
⊢ (𝑎 ∈ On → Pred( E , On,
𝑎) = 𝑎) | 
| 18 | 17 | 3ad2ant1 1133 | . . . . . 6
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) → Pred( E , On,
𝑎) = 𝑎) | 
| 19 |  | predon 7807 | . . . . . . . 8
⊢ (𝑏 ∈ On → Pred( E , On,
𝑏) = 𝑏) | 
| 20 | 19 | 3ad2ant2 1134 | . . . . . . 7
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) → Pred( E , On,
𝑏) = 𝑏) | 
| 21 |  | predon 7807 | . . . . . . . . 9
⊢ (𝑐 ∈ On → Pred( E , On,
𝑐) = 𝑐) | 
| 22 | 21 | 3ad2ant3 1135 | . . . . . . . 8
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) → Pred( E , On,
𝑐) = 𝑐) | 
| 23 | 22 | raleqdv 3325 | . . . . . . 7
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑓 ∈ Pred ( E
, On, 𝑐)𝜃 ↔ ∀𝑓 ∈ 𝑐 𝜃)) | 
| 24 | 20, 23 | raleqbidv 3345 | . . . . . 6
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑒 ∈ Pred ( E
, On, 𝑏)∀𝑓 ∈ Pred ( E , On, 𝑐)𝜃 ↔ ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜃)) | 
| 25 | 18, 24 | raleqbidv 3345 | . . . . 5
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑑 ∈ Pred ( E
, On, 𝑎)∀𝑒 ∈ Pred ( E , On, 𝑏)∀𝑓 ∈ Pred ( E , On, 𝑐)𝜃 ↔ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜃)) | 
| 26 | 20 | raleqdv 3325 | . . . . . 6
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑒 ∈ Pred ( E
, On, 𝑏)𝜒 ↔ ∀𝑒 ∈ 𝑏 𝜒)) | 
| 27 | 18, 26 | raleqbidv 3345 | . . . . 5
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑑 ∈ Pred ( E
, On, 𝑎)∀𝑒 ∈ Pred ( E , On, 𝑏)𝜒 ↔ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ 𝑏 𝜒)) | 
| 28 | 22 | raleqdv 3325 | . . . . . 6
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑓 ∈ Pred ( E
, On, 𝑐)𝜁 ↔ ∀𝑓 ∈ 𝑐 𝜁)) | 
| 29 | 18, 28 | raleqbidv 3345 | . . . . 5
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑑 ∈ Pred ( E
, On, 𝑎)∀𝑓 ∈ Pred ( E , On, 𝑐)𝜁 ↔ ∀𝑑 ∈ 𝑎 ∀𝑓 ∈ 𝑐 𝜁)) | 
| 30 | 25, 27, 29 | 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, 𝑐)𝜁) ↔ (∀𝑑 ∈ 𝑎 ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜃 ∧ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ 𝑏 𝜒 ∧ ∀𝑑 ∈ 𝑎 ∀𝑓 ∈ 𝑐 𝜁))) | 
| 31 | 18 | raleqdv 3325 | . . . . 5
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑑 ∈ Pred ( E
, On, 𝑎)𝜓 ↔ ∀𝑑 ∈ 𝑎 𝜓)) | 
| 32 | 22 | raleqdv 3325 | . . . . . 6
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑓 ∈ Pred ( E
, On, 𝑐)𝜏 ↔ ∀𝑓 ∈ 𝑐 𝜏)) | 
| 33 | 20, 32 | raleqbidv 3345 | . . . . 5
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑒 ∈ Pred ( E
, On, 𝑏)∀𝑓 ∈ Pred ( E , On, 𝑐)𝜏 ↔ ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜏)) | 
| 34 | 20 | raleqdv 3325 | . . . . 5
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑒 ∈ Pred ( E
, On, 𝑏)𝜎 ↔ ∀𝑒 ∈ 𝑏 𝜎)) | 
| 35 | 31, 33, 34 | 3anbi123d 1437 | . . . 4
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
((∀𝑑 ∈ Pred ( E
, On, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred ( E , On, 𝑏)∀𝑓 ∈ Pred ( E , On, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred ( E , On, 𝑏)𝜎) ↔ (∀𝑑 ∈ 𝑎 𝜓 ∧ ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜏 ∧ ∀𝑒 ∈ 𝑏 𝜎))) | 
| 36 | 22 | raleqdv 3325 | . . . 4
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(∀𝑓 ∈ Pred ( E
, On, 𝑐)𝜂 ↔ ∀𝑓 ∈ 𝑐 𝜂)) | 
| 37 | 30, 35, 36 | 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, 𝑐)𝜂) ↔ ((∀𝑑 ∈ 𝑎 ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜃 ∧ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ 𝑏 𝜒 ∧ ∀𝑑 ∈ 𝑎 ∀𝑓 ∈ 𝑐 𝜁) ∧ (∀𝑑 ∈ 𝑎 𝜓 ∧ ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜏 ∧ ∀𝑒 ∈ 𝑏 𝜎) ∧ ∀𝑓 ∈ 𝑐 𝜂))) | 
| 38 |  | on3ind.i | . . 3
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) →
(((∀𝑑 ∈ 𝑎 ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜃 ∧ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ 𝑏 𝜒 ∧ ∀𝑑 ∈ 𝑎 ∀𝑓 ∈ 𝑐 𝜁) ∧ (∀𝑑 ∈ 𝑎 𝜓 ∧ ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜏 ∧ ∀𝑒 ∈ 𝑏 𝜎) ∧ ∀𝑓 ∈ 𝑐 𝜂) → 𝜑)) | 
| 39 | 37, 38 | sylbid 240 | . 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, 𝑐)𝜂) → 𝜑)) | 
| 40 | 1, 5, 6, 1, 5, 6, 1, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 39 | xpord3ind 8182 | 1
⊢ ((𝑋 ∈ On ∧ 𝑌 ∈ On ∧ 𝑍 ∈ On) → 𝜆) |