Step |
Hyp |
Ref |
Expression |
1 |
|
idn1 |
|- (. ( Ord A /\ B e. A ) ->. ( Ord A /\ B e. A ) ). |
2 |
|
simpl |
|- ( ( Ord A /\ B e. A ) -> Ord A ) |
3 |
1 2
|
e1a |
|- (. ( Ord A /\ B e. A ) ->. Ord A ). |
4 |
|
ordtr |
|- ( Ord A -> Tr A ) |
5 |
3 4
|
e1a |
|- (. ( Ord A /\ B e. A ) ->. Tr A ). |
6 |
|
dford2 |
|- ( Ord A <-> ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) ) ) |
7 |
6
|
simprbi |
|- ( Ord A -> A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) ) |
8 |
3 7
|
e1a |
|- (. ( Ord A /\ B e. A ) ->. A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) ). |
9 |
|
3orcomb |
|- ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) ) |
10 |
9
|
ax-gen |
|- A. y ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) ) |
11 |
|
alral |
|- ( A. y ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) ) -> A. y e. A ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) ) ) |
12 |
10 11
|
e0a |
|- A. y e. A ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) ) |
13 |
|
ralbi |
|- ( A. y e. A ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) ) -> ( A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. y e. A ( x e. y \/ y e. x \/ x = y ) ) ) |
14 |
12 13
|
e0a |
|- ( A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. y e. A ( x e. y \/ y e. x \/ x = y ) ) |
15 |
14
|
ax-gen |
|- A. x ( A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. y e. A ( x e. y \/ y e. x \/ x = y ) ) |
16 |
|
alral |
|- ( A. x ( A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. y e. A ( x e. y \/ y e. x \/ x = y ) ) -> A. x e. A ( A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. y e. A ( x e. y \/ y e. x \/ x = y ) ) ) |
17 |
15 16
|
e0a |
|- A. x e. A ( A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. y e. A ( x e. y \/ y e. x \/ x = y ) ) |
18 |
|
ralbi |
|- ( A. x e. A ( A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. y e. A ( x e. y \/ y e. x \/ x = y ) ) -> ( A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) ) ) |
19 |
17 18
|
e0a |
|- ( A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) ) |
20 |
8 19
|
e1bi |
|- (. ( Ord A /\ B e. A ) ->. A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) ). |
21 |
|
simpr |
|- ( ( Ord A /\ B e. A ) -> B e. A ) |
22 |
1 21
|
e1a |
|- (. ( Ord A /\ B e. A ) ->. B e. A ). |
23 |
|
tratrb |
|- ( ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) -> Tr B ) |
24 |
23
|
3exp |
|- ( Tr A -> ( A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) -> ( B e. A -> Tr B ) ) ) |
25 |
5 20 22 24
|
e111 |
|- (. ( Ord A /\ B e. A ) ->. Tr B ). |
26 |
|
trss |
|- ( Tr A -> ( B e. A -> B C_ A ) ) |
27 |
5 22 26
|
e11 |
|- (. ( Ord A /\ B e. A ) ->. B C_ A ). |
28 |
|
ssralv2 |
|- ( ( B C_ A /\ B C_ A ) -> ( A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) -> A. x e. B A. y e. B ( x e. y \/ x = y \/ y e. x ) ) ) |
29 |
28
|
ex |
|- ( B C_ A -> ( B C_ A -> ( A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) -> A. x e. B A. y e. B ( x e. y \/ x = y \/ y e. x ) ) ) ) |
30 |
27 27 8 29
|
e111 |
|- (. ( Ord A /\ B e. A ) ->. A. x e. B A. y e. B ( x e. y \/ x = y \/ y e. x ) ). |
31 |
|
dford2 |
|- ( Ord B <-> ( Tr B /\ A. x e. B A. y e. B ( x e. y \/ x = y \/ y e. x ) ) ) |
32 |
31
|
simplbi2 |
|- ( Tr B -> ( A. x e. B A. y e. B ( x e. y \/ x = y \/ y e. x ) -> Ord B ) ) |
33 |
25 30 32
|
e11 |
|- (. ( Ord A /\ B e. A ) ->. Ord B ). |
34 |
33
|
in1 |
|- ( ( Ord A /\ B e. A ) -> Ord B ) |