Theorem on2ind

Description: Double induction over ordinal numbers. (Contributed by Scott Fenton, 26-Aug-2024)

	Ref	Expression
Hypotheses	on2ind.1	⊢ ( 𝑎 = 𝑐 → ( 𝜑 ↔ 𝜓 ) )
	on2ind.2	⊢ ( 𝑏 = 𝑑 → ( 𝜓 ↔ 𝜒 ) )
	on2ind.3	⊢ ( 𝑎 = 𝑐 → ( 𝜃 ↔ 𝜒 ) )
	on2ind.4	⊢ ( 𝑎 = 𝑋 → ( 𝜑 ↔ 𝜏 ) )
	on2ind.5	⊢ ( 𝑏 = 𝑌 → ( 𝜏 ↔ 𝜂 ) )
	on2ind.i	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 𝜒 ∧ ∀ 𝑐 ∈ 𝑎 𝜓 ∧ ∀ 𝑑 ∈ 𝑏 𝜃 ) → 𝜑 ) )
Assertion	on2ind	⊢ ( ( 𝑋 ∈ On ∧ 𝑌 ∈ On ) → 𝜂 )

Proof

Step	Hyp	Ref	Expression
1		on2ind.1	⊢ ( 𝑎 = 𝑐 → ( 𝜑 ↔ 𝜓 ) )
2		on2ind.2	⊢ ( 𝑏 = 𝑑 → ( 𝜓 ↔ 𝜒 ) )
3		on2ind.3	⊢ ( 𝑎 = 𝑐 → ( 𝜃 ↔ 𝜒 ) )
4		on2ind.4	⊢ ( 𝑎 = 𝑋 → ( 𝜑 ↔ 𝜏 ) )
5		on2ind.5	⊢ ( 𝑏 = 𝑌 → ( 𝜏 ↔ 𝜂 ) )
6		on2ind.i	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 𝜒 ∧ ∀ 𝑐 ∈ 𝑎 𝜓 ∧ ∀ 𝑑 ∈ 𝑏 𝜃 ) → 𝜑 ) )
7		eqid	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1st ‘ 𝑥 ) E ( 1st ‘ 𝑦 ) ∨ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) ∧ ( ( 2nd ‘ 𝑥 ) E ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1st ‘ 𝑥 ) E ( 1st ‘ 𝑦 ) ∨ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) ∧ ( ( 2nd ‘ 𝑥 ) E ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
8		onfr	⊢ E Fr On
9		epweon	⊢ E We On
10		weso	⊢ ( E We On → E Or On )
11		sopo	⊢ ( E Or On → E Po On )
12	9 10 11	mp2b	⊢ E Po On
13		epse	⊢ E Se On
14		predon	⊢ ( 𝑎 ∈ On → Pred ( E , On , 𝑎 ) = 𝑎 )
15	14	adantr	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → Pred ( E , On , 𝑎 ) = 𝑎 )
16		predon	⊢ ( 𝑏 ∈ On → Pred ( E , On , 𝑏 ) = 𝑏 )
17	16	adantl	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → Pred ( E , On , 𝑏 ) = 𝑏 )
18	17	raleqdv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ∀ 𝑑 ∈ Pred ( E , On , 𝑏 ) 𝜒 ↔ ∀ 𝑑 ∈ 𝑏 𝜒 ) )
19	15 18	raleqbidv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ∀ 𝑐 ∈ Pred ( E , On , 𝑎 ) ∀ 𝑑 ∈ Pred ( E , On , 𝑏 ) 𝜒 ↔ ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 𝜒 ) )
20	15	raleqdv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ∀ 𝑐 ∈ Pred ( E , On , 𝑎 ) 𝜓 ↔ ∀ 𝑐 ∈ 𝑎 𝜓 ) )
21	17	raleqdv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ∀ 𝑑 ∈ Pred ( E , On , 𝑏 ) 𝜃 ↔ ∀ 𝑑 ∈ 𝑏 𝜃 ) )
22	19 20 21	3anbi123d	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( ∀ 𝑐 ∈ Pred ( E , On , 𝑎 ) ∀ 𝑑 ∈ Pred ( E , On , 𝑏 ) 𝜒 ∧ ∀ 𝑐 ∈ Pred ( E , On , 𝑎 ) 𝜓 ∧ ∀ 𝑑 ∈ Pred ( E , On , 𝑏 ) 𝜃 ) ↔ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 𝜒 ∧ ∀ 𝑐 ∈ 𝑎 𝜓 ∧ ∀ 𝑑 ∈ 𝑏 𝜃 ) ) )
23	22 6	sylbid	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( ∀ 𝑐 ∈ Pred ( E , On , 𝑎 ) ∀ 𝑑 ∈ Pred ( E , On , 𝑏 ) 𝜒 ∧ ∀ 𝑐 ∈ Pred ( E , On , 𝑎 ) 𝜓 ∧ ∀ 𝑑 ∈ Pred ( E , On , 𝑏 ) 𝜃 ) → 𝜑 ) )
24	7 8 12 13 8 12 13 1 2 3 4 5 23	xpord2ind	⊢ ( ( 𝑋 ∈ On ∧ 𝑌 ∈ On ) → 𝜂 )