Metamath Proof Explorer

Theorem on2ind

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

Ref Expression
Hypotheses on2ind.1 
|- ( a = c -> ( ph <-> ps ) )
on2ind.2 
|- ( b = d -> ( ps <-> ch ) )
on2ind.3 
|- ( a = c -> ( th <-> ch ) )
on2ind.4 
|- ( a = X -> ( ph <-> ta ) )
on2ind.5 
|- ( b = Y -> ( ta <-> et ) )
on2ind.i 
|- ( ( a e. On /\ b e. On ) -> ( ( A. c e. a A. d e. b ch /\ A. c e. a ps /\ A. d e. b th ) -> ph ) )
Assertion on2ind 
|- ( ( X e. On /\ Y e. On ) -> et )

Proof

Step Hyp Ref Expression
1 on2ind.1 
 |-  ( a = c -> ( ph <-> ps ) )
2 on2ind.2 
 |-  ( b = d -> ( ps <-> ch ) )
3 on2ind.3 
 |-  ( a = c -> ( th <-> ch ) )
4 on2ind.4 
 |-  ( a = X -> ( ph <-> ta ) )
5 on2ind.5 
 |-  ( b = Y -> ( ta <-> et ) )
6 on2ind.i 
 |-  ( ( a e. On /\ b e. On ) -> ( ( A. c e. a A. d e. b ch /\ A. c e. a ps /\ A. d e. b th ) -> ph ) )
7 eqid 
 |-  { <. x , y >. | ( x e. ( On X. On ) /\ y e. ( On X. On ) /\ ( ( ( 1st ` x ) _E ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) ) /\ ( ( 2nd ` x ) _E ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) } = { <. x , y >. | ( x e. ( On X. On ) /\ y e. ( On X. On ) /\ ( ( ( 1st ` x ) _E ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) ) /\ ( ( 2nd ` x ) _E ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) }
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 
 |-  ( a e. On -> Pred ( _E , On , a ) = a )
15 14 adantr 
 |-  ( ( a e. On /\ b e. On ) -> Pred ( _E , On , a ) = a )
16 predon 
 |-  ( b e. On -> Pred ( _E , On , b ) = b )
17 16 adantl 
 |-  ( ( a e. On /\ b e. On ) -> Pred ( _E , On , b ) = b )
18 17 raleqdv 
 |-  ( ( a e. On /\ b e. On ) -> ( A. d e. Pred ( _E , On , b ) ch <-> A. d e. b ch ) )
19 15 18 raleqbidv 
 |-  ( ( a e. On /\ b e. On ) -> ( A. c e. Pred ( _E , On , a ) A. d e. Pred ( _E , On , b ) ch <-> A. c e. a A. d e. b ch ) )
20 15 raleqdv 
 |-  ( ( a e. On /\ b e. On ) -> ( A. c e. Pred ( _E , On , a ) ps <-> A. c e. a ps ) )
21 17 raleqdv 
 |-  ( ( a e. On /\ b e. On ) -> ( A. d e. Pred ( _E , On , b ) th <-> A. d e. b th ) )
22 19 20 21 3anbi123d 
 |-  ( ( a e. On /\ b e. On ) -> ( ( A. c e. Pred ( _E , On , a ) A. d e. Pred ( _E , On , b ) ch /\ A. c e. Pred ( _E , On , a ) ps /\ A. d e. Pred ( _E , On , b ) th ) <-> ( A. c e. a A. d e. b ch /\ A. c e. a ps /\ A. d e. b th ) ) )
23 22 6 sylbid 
 |-  ( ( a e. On /\ b e. On ) -> ( ( A. c e. Pred ( _E , On , a ) A. d e. Pred ( _E , On , b ) ch /\ A. c e. Pred ( _E , On , a ) ps /\ A. d e. Pred ( _E , On , b ) th ) -> ph ) )
24 7 8 12 13 8 12 13 1 2 3 4 5 23 xpord2ind 
 |-  ( ( X e. On /\ Y e. On ) -> et )