Metamath Proof Explorer

Theorem satf0op

Description: An element of a value of the satisfaction predicate as function over wff codes in the empty model and the empty binary relation expressed as ordered pair. (Contributed by AV, 19-Sep-2023)

Ref Expression
Hypothesis satf0op.s 
|- S = ( (/) Sat (/) )
Assertion satf0op 
|- ( N e. _om -> ( X e. ( S ` N ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` N ) ) ) )

Proof

Step Hyp Ref Expression
1 satf0op.s 
 |-  S = ( (/) Sat (/) )
2 fveq2 
 |-  ( y = (/) -> ( S ` y ) = ( S ` (/) ) )
3 2 eleq2d 
 |-  ( y = (/) -> ( X e. ( S ` y ) <-> X e. ( S ` (/) ) ) )
4 2 eleq2d 
 |-  ( y = (/) -> ( <. x , (/) >. e. ( S ` y ) <-> <. x , (/) >. e. ( S ` (/) ) ) )
5 4 anbi2d 
 |-  ( y = (/) -> ( ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` y ) ) <-> ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` (/) ) ) ) )
6 5 exbidv 
 |-  ( y = (/) -> ( E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` y ) ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` (/) ) ) ) )
7 3 6 bibi12d 
 |-  ( y = (/) -> ( ( X e. ( S ` y ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` y ) ) ) <-> ( X e. ( S ` (/) ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` (/) ) ) ) ) )
8 fveq2 
 |-  ( y = z -> ( S ` y ) = ( S ` z ) )
9 8 eleq2d 
 |-  ( y = z -> ( X e. ( S ` y ) <-> X e. ( S ` z ) ) )
10 8 eleq2d 
 |-  ( y = z -> ( <. x , (/) >. e. ( S ` y ) <-> <. x , (/) >. e. ( S ` z ) ) )
11 10 anbi2d 
 |-  ( y = z -> ( ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` y ) ) <-> ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` z ) ) ) )
12 11 exbidv 
 |-  ( y = z -> ( E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` y ) ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` z ) ) ) )
13 9 12 bibi12d 
 |-  ( y = z -> ( ( X e. ( S ` y ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` y ) ) ) <-> ( X e. ( S ` z ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` z ) ) ) ) )
14 fveq2 
 |-  ( y = suc z -> ( S ` y ) = ( S ` suc z ) )
15 14 eleq2d 
 |-  ( y = suc z -> ( X e. ( S ` y ) <-> X e. ( S ` suc z ) ) )
16 14 eleq2d 
 |-  ( y = suc z -> ( <. x , (/) >. e. ( S ` y ) <-> <. x , (/) >. e. ( S ` suc z ) ) )
17 16 anbi2d 
 |-  ( y = suc z -> ( ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` y ) ) <-> ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` suc z ) ) ) )
18 17 exbidv 
 |-  ( y = suc z -> ( E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` y ) ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` suc z ) ) ) )
19 15 18 bibi12d 
 |-  ( y = suc z -> ( ( X e. ( S ` y ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` y ) ) ) <-> ( X e. ( S ` suc z ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` suc z ) ) ) ) )
20 fveq2 
 |-  ( y = N -> ( S ` y ) = ( S ` N ) )
21 20 eleq2d 
 |-  ( y = N -> ( X e. ( S ` y ) <-> X e. ( S ` N ) ) )
22 20 eleq2d 
 |-  ( y = N -> ( <. x , (/) >. e. ( S ` y ) <-> <. x , (/) >. e. ( S ` N ) ) )
23 22 anbi2d 
 |-  ( y = N -> ( ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` y ) ) <-> ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` N ) ) ) )
24 23 exbidv 
 |-  ( y = N -> ( E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` y ) ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` N ) ) ) )
25 21 24 bibi12d 
 |-  ( y = N -> ( ( X e. ( S ` y ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` y ) ) ) <-> ( X e. ( S ` N ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` N ) ) ) ) )
26 1 fveq1i 
 |-  ( S ` (/) ) = ( ( (/) Sat (/) ) ` (/) )
27 satf00 
 |-  ( ( (/) Sat (/) ) ` (/) ) = { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) }
28 26 27 eqtri 
 |-  ( S ` (/) ) = { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) }
29 28 eleq2i 
 |-  ( X e. ( S ` (/) ) <-> X e. { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } )
30 elopab 
 |-  ( X e. { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } <-> E. x E. y ( X = <. x , y >. /\ ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) ) )
31 opeq2 
 |-  ( y = (/) -> <. x , y >. = <. x , (/) >. )
32 31 adantr 
 |-  ( ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) -> <. x , y >. = <. x , (/) >. )
33 32 eqeq2d 
 |-  ( ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) -> ( X = <. x , y >. <-> X = <. x , (/) >. ) )
34 33 biimpd 
 |-  ( ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) -> ( X = <. x , y >. -> X = <. x , (/) >. ) )
35 34 impcom 
 |-  ( ( X = <. x , y >. /\ ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) ) -> X = <. x , (/) >. )
36 eqidd 
 |-  ( y = (/) -> (/) = (/) )
37 36 anim1i 
 |-  ( ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) -> ( (/) = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) )
38 37 adantl 
 |-  ( ( X = <. x , y >. /\ ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) ) -> ( (/) = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) )
39 satf00 
 |-  ( ( (/) Sat (/) ) ` (/) ) = { <. y , z >. | ( z = (/) /\ E. i e. _om E. j e. _om y = ( i e.g j ) ) }
40 26 39 eqtri 
 |-  ( S ` (/) ) = { <. y , z >. | ( z = (/) /\ E. i e. _om E. j e. _om y = ( i e.g j ) ) }
41 40 eleq2i 
 |-  ( <. x , (/) >. e. ( S ` (/) ) <-> <. x , (/) >. e. { <. y , z >. | ( z = (/) /\ E. i e. _om E. j e. _om y = ( i e.g j ) ) } )
42 vex 
 |-  x e. _V
43 0ex 
 |-  (/) e. _V
44 eqeq1 
 |-  ( z = (/) -> ( z = (/) <-> (/) = (/) ) )
45 eqeq1 
 |-  ( y = x -> ( y = ( i e.g j ) <-> x = ( i e.g j ) ) )
46 45 2rexbidv 
 |-  ( y = x -> ( E. i e. _om E. j e. _om y = ( i e.g j ) <-> E. i e. _om E. j e. _om x = ( i e.g j ) ) )
47 44 46 bi2anan9r 
 |-  ( ( y = x /\ z = (/) ) -> ( ( z = (/) /\ E. i e. _om E. j e. _om y = ( i e.g j ) ) <-> ( (/) = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) ) )
48 42 43 47 opelopaba 
 |-  ( <. x , (/) >. e. { <. y , z >. | ( z = (/) /\ E. i e. _om E. j e. _om y = ( i e.g j ) ) } <-> ( (/) = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) )
49 41 48 bitri 
 |-  ( <. x , (/) >. e. ( S ` (/) ) <-> ( (/) = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) )
50 38 49 sylibr 
 |-  ( ( X = <. x , y >. /\ ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) ) -> <. x , (/) >. e. ( S ` (/) ) )
51 35 50 jca 
 |-  ( ( X = <. x , y >. /\ ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) ) -> ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` (/) ) ) )
52 51 exlimiv 
 |-  ( E. y ( X = <. x , y >. /\ ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) ) -> ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` (/) ) ) )
53 31 eqeq2d 
 |-  ( y = (/) -> ( X = <. x , y >. <-> X = <. x , (/) >. ) )
54 eqeq1 
 |-  ( y = (/) -> ( y = (/) <-> (/) = (/) ) )
55 54 anbi1d 
 |-  ( y = (/) -> ( ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) <-> ( (/) = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) ) )
56 53 55 anbi12d 
 |-  ( y = (/) -> ( ( X = <. x , y >. /\ ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) ) <-> ( X = <. x , (/) >. /\ ( (/) = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) ) ) )
57 43 56 spcev 
 |-  ( ( X = <. x , (/) >. /\ ( (/) = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) ) -> E. y ( X = <. x , y >. /\ ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) ) )
58 49 57 sylan2b 
 |-  ( ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` (/) ) ) -> E. y ( X = <. x , y >. /\ ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) ) )
59 52 58 impbii 
 |-  ( E. y ( X = <. x , y >. /\ ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) ) <-> ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` (/) ) ) )
60 59 exbii 
 |-  ( E. x E. y ( X = <. x , y >. /\ ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` (/) ) ) )
61 29 30 60 3bitri 
 |-  ( X e. ( S ` (/) ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` (/) ) ) )
62 1 satf0suc 
 |-  ( z e. _om -> ( S ` suc z ) = ( ( S ` z ) u. { <. a , b >. | ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) } ) )
63 62 eleq2d 
 |-  ( z e. _om -> ( X e. ( S ` suc z ) <-> X e. ( ( S ` z ) u. { <. a , b >. | ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) } ) ) )
64 elun 
 |-  ( X e. ( ( S ` z ) u. { <. a , b >. | ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) } ) <-> ( X e. ( S ` z ) \/ X e. { <. a , b >. | ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) } ) )
65 64 a1i 
 |-  ( z e. _om -> ( X e. ( ( S ` z ) u. { <. a , b >. | ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) } ) <-> ( X e. ( S ` z ) \/ X e. { <. a , b >. | ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) } ) ) )
66 elopab 
 |-  ( X e. { <. a , b >. | ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) } <-> E. a E. b ( X = <. a , b >. /\ ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) )
67 66 a1i 
 |-  ( z e. _om -> ( X e. { <. a , b >. | ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) } <-> E. a E. b ( X = <. a , b >. /\ ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) ) )
68 67 orbi2d 
 |-  ( z e. _om -> ( ( X e. ( S ` z ) \/ X e. { <. a , b >. | ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) } ) <-> ( X e. ( S ` z ) \/ E. a E. b ( X = <. a , b >. /\ ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) ) ) )
69 63 65 68 3bitrd 
 |-  ( z e. _om -> ( X e. ( S ` suc z ) <-> ( X e. ( S ` z ) \/ E. a E. b ( X = <. a , b >. /\ ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) ) ) )
70 69 adantr 
 |-  ( ( z e. _om /\ ( X e. ( S ` z ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` z ) ) ) ) -> ( X e. ( S ` suc z ) <-> ( X e. ( S ` z ) \/ E. a E. b ( X = <. a , b >. /\ ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) ) ) )
71 simpr 
 |-  ( ( z e. _om /\ ( X e. ( S ` z ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` z ) ) ) ) -> ( X e. ( S ` z ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` z ) ) ) )
72 opeq2 
 |-  ( b = (/) -> <. a , b >. = <. a , (/) >. )
73 72 eqeq2d 
 |-  ( b = (/) -> ( X = <. a , b >. <-> X = <. a , (/) >. ) )
74 73 biimpd 
 |-  ( b = (/) -> ( X = <. a , b >. -> X = <. a , (/) >. ) )
75 74 adantr 
 |-  ( ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) -> ( X = <. a , b >. -> X = <. a , (/) >. ) )
76 75 impcom 
 |-  ( ( X = <. a , b >. /\ ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) -> X = <. a , (/) >. )
77 eqidd 
 |-  ( ( X = <. a , b >. /\ ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) -> (/) = (/) )
78 simpr 
 |-  ( ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) -> E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) )
79 78 adantl 
 |-  ( ( X = <. a , b >. /\ ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) -> E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) )
80 77 79 jca 
 |-  ( ( X = <. a , b >. /\ ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) -> ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) )
81 76 80 jca 
 |-  ( ( X = <. a , b >. /\ ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) -> ( X = <. a , (/) >. /\ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) )
82 81 exlimiv 
 |-  ( E. b ( X = <. a , b >. /\ ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) -> ( X = <. a , (/) >. /\ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) )
83 eqeq1 
 |-  ( b = (/) -> ( b = (/) <-> (/) = (/) ) )
84 83 anbi1d 
 |-  ( b = (/) -> ( ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) <-> ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) )
85 73 84 anbi12d 
 |-  ( b = (/) -> ( ( X = <. a , b >. /\ ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) <-> ( X = <. a , (/) >. /\ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) ) )
86 43 85 spcev 
 |-  ( ( X = <. a , (/) >. /\ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) -> E. b ( X = <. a , b >. /\ ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) )
87 82 86 impbii 
 |-  ( E. b ( X = <. a , b >. /\ ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) <-> ( X = <. a , (/) >. /\ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) )
88 87 exbii 
 |-  ( E. a E. b ( X = <. a , b >. /\ ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) <-> E. a ( X = <. a , (/) >. /\ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) )
89 88 a1i 
 |-  ( z e. _om -> ( E. a E. b ( X = <. a , b >. /\ ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) <-> E. a ( X = <. a , (/) >. /\ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) ) )
90 opeq1 
 |-  ( x = a -> <. x , (/) >. = <. a , (/) >. )
91 90 eqeq2d 
 |-  ( x = a -> ( X = <. x , (/) >. <-> X = <. a , (/) >. ) )
92 eqeq1 
 |-  ( x = a -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) <-> a = ( ( 1st ` u ) |g ( 1st ` v ) ) ) )
93 92 rexbidv 
 |-  ( x = a -> ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) <-> E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) ) )
94 eqeq1 
 |-  ( x = a -> ( x = A.g i ( 1st ` u ) <-> a = A.g i ( 1st ` u ) ) )
95 94 rexbidv 
 |-  ( x = a -> ( E. i e. _om x = A.g i ( 1st ` u ) <-> E. i e. _om a = A.g i ( 1st ` u ) ) )
96 93 95 orbi12d 
 |-  ( x = a -> ( ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) <-> ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) )
97 96 rexbidv 
 |-  ( x = a -> ( E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) <-> E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) )
98 97 anbi2d 
 |-  ( x = a -> ( ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) <-> ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) )
99 91 98 anbi12d 
 |-  ( x = a -> ( ( X = <. x , (/) >. /\ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) <-> ( X = <. a , (/) >. /\ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) ) )
100 99 cbvexvw 
 |-  ( E. x ( X = <. x , (/) >. /\ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) <-> E. a ( X = <. a , (/) >. /\ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) )
101 89 100 bitr4di 
 |-  ( z e. _om -> ( E. a E. b ( X = <. a , b >. /\ ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) <-> E. x ( X = <. x , (/) >. /\ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) ) )
102 101 adantr 
 |-  ( ( z e. _om /\ ( X e. ( S ` z ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` z ) ) ) ) -> ( E. a E. b ( X = <. a , b >. /\ ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) <-> E. x ( X = <. x , (/) >. /\ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) ) )
103 71 102 orbi12d 
 |-  ( ( z e. _om /\ ( X e. ( S ` z ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` z ) ) ) ) -> ( ( X e. ( S ` z ) \/ E. a E. b ( X = <. a , b >. /\ ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) ) <-> ( E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` z ) ) \/ E. x ( X = <. x , (/) >. /\ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) ) ) )
104 19.43 
 |-  ( E. x ( ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` z ) ) \/ ( X = <. x , (/) >. /\ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) ) <-> ( E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` z ) ) \/ E. x ( X = <. x , (/) >. /\ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) ) )
105 andi 
 |-  ( ( X = <. x , (/) >. /\ ( <. x , (/) >. e. ( S ` z ) \/ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) ) <-> ( ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` z ) ) \/ ( X = <. x , (/) >. /\ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) ) )
106 105 bicomi 
 |-  ( ( ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` z ) ) \/ ( X = <. x , (/) >. /\ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) ) <-> ( X = <. x , (/) >. /\ ( <. x , (/) >. e. ( S ` z ) \/ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) ) )
107 106 exbii 
 |-  ( E. x ( ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` z ) ) \/ ( X = <. x , (/) >. /\ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) ) <-> E. x ( X = <. x , (/) >. /\ ( <. x , (/) >. e. ( S ` z ) \/ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) ) )
108 104 107 bitr3i 
 |-  ( ( E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` z ) ) \/ E. x ( X = <. x , (/) >. /\ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) ) <-> E. x ( X = <. x , (/) >. /\ ( <. x , (/) >. e. ( S ` z ) \/ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) ) )
109 103 108 bitrdi 
 |-  ( ( z e. _om /\ ( X e. ( S ` z ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` z ) ) ) ) -> ( ( X e. ( S ` z ) \/ E. a E. b ( X = <. a , b >. /\ ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) ) ) <-> E. x ( X = <. x , (/) >. /\ ( <. x , (/) >. e. ( S ` z ) \/ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) ) ) )
110 62 eleq2d 
 |-  ( z e. _om -> ( <. x , (/) >. e. ( S ` suc z ) <-> <. x , (/) >. e. ( ( S ` z ) u. { <. a , b >. | ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) } ) ) )
111 elun 
 |-  ( <. x , (/) >. e. ( ( S ` z ) u. { <. a , b >. | ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) } ) <-> ( <. x , (/) >. e. ( S ` z ) \/ <. x , (/) >. e. { <. a , b >. | ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) } ) )
112 eqeq1 
 |-  ( a = x -> ( a = ( ( 1st ` u ) |g ( 1st ` v ) ) <-> x = ( ( 1st ` u ) |g ( 1st ` v ) ) ) )
113 112 rexbidv 
 |-  ( a = x -> ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) <-> E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) ) )
114 eqeq1 
 |-  ( a = x -> ( a = A.g i ( 1st ` u ) <-> x = A.g i ( 1st ` u ) ) )
115 114 rexbidv 
 |-  ( a = x -> ( E. i e. _om a = A.g i ( 1st ` u ) <-> E. i e. _om x = A.g i ( 1st ` u ) ) )
116 113 115 orbi12d 
 |-  ( a = x -> ( ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) <-> ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) )
117 116 rexbidv 
 |-  ( a = x -> ( E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) <-> E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) )
118 83 117 bi2anan9r 
 |-  ( ( a = x /\ b = (/) ) -> ( ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) <-> ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) )
119 42 43 118 opelopaba 
 |-  ( <. x , (/) >. e. { <. a , b >. | ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) } <-> ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) )
120 119 orbi2i 
 |-  ( ( <. x , (/) >. e. ( S ` z ) \/ <. x , (/) >. e. { <. a , b >. | ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) } ) <-> ( <. x , (/) >. e. ( S ` z ) \/ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) )
121 111 120 bitri 
 |-  ( <. x , (/) >. e. ( ( S ` z ) u. { <. a , b >. | ( b = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) a = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om a = A.g i ( 1st ` u ) ) ) } ) <-> ( <. x , (/) >. e. ( S ` z ) \/ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) )
122 110 121 bitrdi 
 |-  ( z e. _om -> ( <. x , (/) >. e. ( S ` suc z ) <-> ( <. x , (/) >. e. ( S ` z ) \/ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) ) )
123 122 anbi2d 
 |-  ( z e. _om -> ( ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` suc z ) ) <-> ( X = <. x , (/) >. /\ ( <. x , (/) >. e. ( S ` z ) \/ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) ) ) )
124 123 exbidv 
 |-  ( z e. _om -> ( E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` suc z ) ) <-> E. x ( X = <. x , (/) >. /\ ( <. x , (/) >. e. ( S ` z ) \/ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) ) ) )
125 124 bicomd 
 |-  ( z e. _om -> ( E. x ( X = <. x , (/) >. /\ ( <. x , (/) >. e. ( S ` z ) \/ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` suc z ) ) ) )
126 125 adantr 
 |-  ( ( z e. _om /\ ( X e. ( S ` z ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` z ) ) ) ) -> ( E. x ( X = <. x , (/) >. /\ ( <. x , (/) >. e. ( S ` z ) \/ ( (/) = (/) /\ E. u e. ( S ` z ) ( E. v e. ( S ` z ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` suc z ) ) ) )
127 70 109 126 3bitrd 
 |-  ( ( z e. _om /\ ( X e. ( S ` z ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` z ) ) ) ) -> ( X e. ( S ` suc z ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` suc z ) ) ) )
128 127 ex 
 |-  ( z e. _om -> ( ( X e. ( S ` z ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` z ) ) ) -> ( X e. ( S ` suc z ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` suc z ) ) ) ) )
129 7 13 19 25 61 128 finds 
 |-  ( N e. _om -> ( X e. ( S ` N ) <-> E. x ( X = <. x , (/) >. /\ <. x , (/) >. e. ( S ` N ) ) ) )