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 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 
 |-  ( a e. On -> Pred ( _E , On , a ) = a )
14 13 adantr 
 |-  ( ( a e. On /\ b e. On ) -> Pred ( _E , On , a ) = a )
15 predon 
 |-  ( b e. On -> Pred ( _E , On , b ) = b )
16 15 adantl 
 |-  ( ( a e. On /\ b e. On ) -> Pred ( _E , On , b ) = b )
17 16 raleqdv 
 |-  ( ( a e. On /\ b e. On ) -> ( A. d e. Pred ( _E , On , b ) ch <-> A. d e. b ch ) )
18 14 17 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 ) )
19 14 raleqdv 
 |-  ( ( a e. On /\ b e. On ) -> ( A. c e. Pred ( _E , On , a ) ps <-> A. c e. a ps ) )
20 16 raleqdv 
 |-  ( ( a e. On /\ b e. On ) -> ( A. d e. Pred ( _E , On , b ) th <-> A. d e. b th ) )
21 18 19 20 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 ) ) )
22 21 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 ) )
23 7 11 12 7 11 12 1 2 3 4 5 22 xpord2ind 
 |-  ( ( X e. On /\ Y e. On ) -> et )