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		onfr	⊢ E Fr On
8		epweon	⊢ E We On
9		weso	⊢ ( E We On → E Or On )
10		sopo	⊢ ( E Or On → E Po On )
11	8 9 10	mp2b	⊢ E Po On
12		epse	⊢ E Se On
13		predon	⊢ ( 𝑎 ∈ On → Pred ( E , On , 𝑎 ) = 𝑎 )
14	13	adantr	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → Pred ( E , On , 𝑎 ) = 𝑎 )
15		predon	⊢ ( 𝑏 ∈ On → Pred ( E , On , 𝑏 ) = 𝑏 )
16	15	adantl	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → Pred ( E , On , 𝑏 ) = 𝑏 )
17	16	raleqdv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ∀ 𝑑 ∈ Pred ( E , On , 𝑏 ) 𝜒 ↔ ∀ 𝑑 ∈ 𝑏 𝜒 ) )
18	14 17	raleqbidv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ∀ 𝑐 ∈ Pred ( E , On , 𝑎 ) ∀ 𝑑 ∈ Pred ( E , On , 𝑏 ) 𝜒 ↔ ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 𝜒 ) )
19	14	raleqdv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ∀ 𝑐 ∈ Pred ( E , On , 𝑎 ) 𝜓 ↔ ∀ 𝑐 ∈ 𝑎 𝜓 ) )
20	16	raleqdv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ∀ 𝑑 ∈ Pred ( E , On , 𝑏 ) 𝜃 ↔ ∀ 𝑑 ∈ 𝑏 𝜃 ) )
21	18 19 20	3anbi123d	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( ∀ 𝑐 ∈ Pred ( E , On , 𝑎 ) ∀ 𝑑 ∈ Pred ( E , On , 𝑏 ) 𝜒 ∧ ∀ 𝑐 ∈ Pred ( E , On , 𝑎 ) 𝜓 ∧ ∀ 𝑑 ∈ Pred ( E , On , 𝑏 ) 𝜃 ) ↔ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 𝜒 ∧ ∀ 𝑐 ∈ 𝑎 𝜓 ∧ ∀ 𝑑 ∈ 𝑏 𝜃 ) ) )
22	21 6	sylbid	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( ∀ 𝑐 ∈ Pred ( E , On , 𝑎 ) ∀ 𝑑 ∈ Pred ( E , On , 𝑏 ) 𝜒 ∧ ∀ 𝑐 ∈ Pred ( E , On , 𝑎 ) 𝜓 ∧ ∀ 𝑑 ∈ Pred ( E , On , 𝑏 ) 𝜃 ) → 𝜑 ) )
23	7 11 12 7 11 12 1 2 3 4 5 22	xpord2ind	⊢ ( ( 𝑋 ∈ On ∧ 𝑌 ∈ On ) → 𝜂 )