ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  recexprlem1ssu Structured version   GIF version

Theorem recexprlem1ssu 6458
Description: The upper cut of one is a subset of the upper cut of A ·P B. Lemma for recexpr 6462. (Contributed by Jim Kingdon, 27-Dec-2019.)
Hypothesis
Ref Expression
recexpr.1 B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩
Assertion
Ref Expression
recexprlem1ssu (A P → (2nd ‘1P) ⊆ (2nd ‘(A ·P B)))
Distinct variable groups:   x,y,A   x,B,y

Proof of Theorem recexprlem1ssu
Dummy variables z w v u f g are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1pru 6395 . . . 4 (2nd ‘1P) = {w ∣ 1Q <Q w}
21abeq2i 2124 . . 3 (w (2nd ‘1P) ↔ 1Q <Q w)
3 prop 6318 . . . . . 6 (A P → ⟨(1stA), (2ndA)⟩ P)
4 prmuloc2 6400 . . . . . 6 ((⟨(1stA), (2ndA)⟩ P 1Q <Q w) → v (1stA)(v ·Q w) (2ndA))
53, 4sylan 267 . . . . 5 ((A P 1Q <Q w) → v (1stA)(v ·Q w) (2ndA))
6 prnminu 6332 . . . . . . . 8 ((⟨(1stA), (2ndA)⟩ P (v ·Q w) (2ndA)) → z (2ndA)z <Q (v ·Q w))
73, 6sylan 267 . . . . . . 7 ((A P (v ·Q w) (2ndA)) → z (2ndA)z <Q (v ·Q w))
87ad2ant2rl 465 . . . . . 6 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA))) → z (2ndA)z <Q (v ·Q w))
9 simp3 890 . . . . . . . . . . 11 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → z <Q (v ·Q w))
10 simp2l 914 . . . . . . . . . . . 12 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → v (1stA))
11 elprnql 6324 . . . . . . . . . . . . . . . . . 18 ((⟨(1stA), (2ndA)⟩ P v (1stA)) → v Q)
123, 11sylan 267 . . . . . . . . . . . . . . . . 17 ((A P v (1stA)) → v Q)
1312ad2ant2r 463 . . . . . . . . . . . . . . . 16 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA))) → v Q)
14133adant3 908 . . . . . . . . . . . . . . 15 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → v Q)
15 simp1r 913 . . . . . . . . . . . . . . . 16 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → 1Q <Q w)
16 ltrelnq 6213 . . . . . . . . . . . . . . . . . 18 <Q ⊆ (Q × Q)
1716brel 4310 . . . . . . . . . . . . . . . . 17 (1Q <Q w → (1Q Q w Q))
1817simprd 107 . . . . . . . . . . . . . . . 16 (1Q <Q ww Q)
1915, 18syl 14 . . . . . . . . . . . . . . 15 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → w Q)
20 recclnq 6240 . . . . . . . . . . . . . . . 16 (w Q → (*Qw) Q)
2119, 20syl 14 . . . . . . . . . . . . . . 15 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (*Qw) Q)
22 mulassnqg 6232 . . . . . . . . . . . . . . 15 ((v Q w Q (*Qw) Q) → ((v ·Q w) ·Q (*Qw)) = (v ·Q (w ·Q (*Qw))))
2314, 19, 21, 22syl3anc 1118 . . . . . . . . . . . . . 14 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((v ·Q w) ·Q (*Qw)) = (v ·Q (w ·Q (*Qw))))
24 recidnq 6241 . . . . . . . . . . . . . . . 16 (w Q → (w ·Q (*Qw)) = 1Q)
2519, 24syl 14 . . . . . . . . . . . . . . 15 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (w ·Q (*Qw)) = 1Q)
2625oveq2d 5443 . . . . . . . . . . . . . 14 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (v ·Q (w ·Q (*Qw))) = (v ·Q 1Q))
27 mulidnq 6237 . . . . . . . . . . . . . . 15 (v Q → (v ·Q 1Q) = v)
2814, 27syl 14 . . . . . . . . . . . . . 14 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (v ·Q 1Q) = v)
2923, 26, 283eqtrd 2052 . . . . . . . . . . . . 13 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((v ·Q w) ·Q (*Qw)) = v)
3029eleq1d 2082 . . . . . . . . . . . 12 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (((v ·Q w) ·Q (*Qw)) (1stA) ↔ v (1stA)))
3110, 30mpbird 156 . . . . . . . . . . 11 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((v ·Q w) ·Q (*Qw)) (1stA))
32 ltrnqi 6267 . . . . . . . . . . . . 13 (z <Q (v ·Q w) → (*Q‘(v ·Q w)) <Q (*Qz))
33 ltmnqg 6249 . . . . . . . . . . . . . . 15 ((f Q g Q Q) → (f <Q g ↔ ( ·Q f) <Q ( ·Q g)))
3433adantl 262 . . . . . . . . . . . . . 14 ((((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) (f Q g Q Q)) → (f <Q g ↔ ( ·Q f) <Q ( ·Q g)))
35 mulclnq 6224 . . . . . . . . . . . . . . . 16 ((v Q w Q) → (v ·Q w) Q)
3614, 19, 35syl2anc 391 . . . . . . . . . . . . . . 15 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (v ·Q w) Q)
37 recclnq 6240 . . . . . . . . . . . . . . 15 ((v ·Q w) Q → (*Q‘(v ·Q w)) Q)
3836, 37syl 14 . . . . . . . . . . . . . 14 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (*Q‘(v ·Q w)) Q)
3916brel 4310 . . . . . . . . . . . . . . . . 17 (z <Q (v ·Q w) → (z Q (v ·Q w) Q))
4039simpld 105 . . . . . . . . . . . . . . . 16 (z <Q (v ·Q w) → z Q)
419, 40syl 14 . . . . . . . . . . . . . . 15 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → z Q)
42 recclnq 6240 . . . . . . . . . . . . . . 15 (z Q → (*Qz) Q)
4341, 42syl 14 . . . . . . . . . . . . . 14 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (*Qz) Q)
44 mulcomnqg 6231 . . . . . . . . . . . . . . 15 ((f Q g Q) → (f ·Q g) = (g ·Q f))
4544adantl 262 . . . . . . . . . . . . . 14 ((((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) (f Q g Q)) → (f ·Q g) = (g ·Q f))
4634, 38, 43, 19, 45caovord2d 5584 . . . . . . . . . . . . 13 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((*Q‘(v ·Q w)) <Q (*Qz) ↔ ((*Q‘(v ·Q w)) ·Q w) <Q ((*Qz) ·Q w)))
4732, 46syl5ib 143 . . . . . . . . . . . 12 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (z <Q (v ·Q w) → ((*Q‘(v ·Q w)) ·Q w) <Q ((*Qz) ·Q w)))
48 1nq 6214 . . . . . . . . . . . . . . . . 17 1Q Q
49 mulidnq 6237 . . . . . . . . . . . . . . . . 17 (1Q Q → (1Q ·Q 1Q) = 1Q)
5048, 49ax-mp 7 . . . . . . . . . . . . . . . 16 (1Q ·Q 1Q) = 1Q
51 mulcomnqg 6231 . . . . . . . . . . . . . . . . . . . . 21 (((v ·Q w) Q (*Q‘(v ·Q w)) Q) → ((v ·Q w) ·Q (*Q‘(v ·Q w))) = ((*Q‘(v ·Q w)) ·Q (v ·Q w)))
5237, 51mpdan 398 . . . . . . . . . . . . . . . . . . . 20 ((v ·Q w) Q → ((v ·Q w) ·Q (*Q‘(v ·Q w))) = ((*Q‘(v ·Q w)) ·Q (v ·Q w)))
53 recidnq 6241 . . . . . . . . . . . . . . . . . . . 20 ((v ·Q w) Q → ((v ·Q w) ·Q (*Q‘(v ·Q w))) = 1Q)
5452, 53eqtr3d 2050 . . . . . . . . . . . . . . . . . . 19 ((v ·Q w) Q → ((*Q‘(v ·Q w)) ·Q (v ·Q w)) = 1Q)
5554, 24oveqan12d 5446 . . . . . . . . . . . . . . . . . 18 (((v ·Q w) Q w Q) → (((*Q‘(v ·Q w)) ·Q (v ·Q w)) ·Q (w ·Q (*Qw))) = (1Q ·Q 1Q))
5636, 19, 55syl2anc 391 . . . . . . . . . . . . . . . . 17 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (((*Q‘(v ·Q w)) ·Q (v ·Q w)) ·Q (w ·Q (*Qw))) = (1Q ·Q 1Q))
57 mulassnqg 6232 . . . . . . . . . . . . . . . . . . 19 ((f Q g Q Q) → ((f ·Q g) ·Q ) = (f ·Q (g ·Q )))
5857adantl 262 . . . . . . . . . . . . . . . . . 18 ((((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) (f Q g Q Q)) → ((f ·Q g) ·Q ) = (f ·Q (g ·Q )))
59 mulclnq 6224 . . . . . . . . . . . . . . . . . . 19 ((f Q g Q) → (f ·Q g) Q)
6059adantl 262 . . . . . . . . . . . . . . . . . 18 ((((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) (f Q g Q)) → (f ·Q g) Q)
6138, 36, 19, 45, 58, 21, 60caov4d 5599 . . . . . . . . . . . . . . . . 17 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (((*Q‘(v ·Q w)) ·Q (v ·Q w)) ·Q (w ·Q (*Qw))) = (((*Q‘(v ·Q w)) ·Q w) ·Q ((v ·Q w) ·Q (*Qw))))
6256, 61eqtr3d 2050 . . . . . . . . . . . . . . . 16 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (1Q ·Q 1Q) = (((*Q‘(v ·Q w)) ·Q w) ·Q ((v ·Q w) ·Q (*Qw))))
6350, 62syl5reqr 2063 . . . . . . . . . . . . . . 15 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (((*Q‘(v ·Q w)) ·Q w) ·Q ((v ·Q w) ·Q (*Qw))) = 1Q)
6460, 38, 19caovcld 5568 . . . . . . . . . . . . . . . 16 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((*Q‘(v ·Q w)) ·Q w) Q)
6560, 36, 21caovcld 5568 . . . . . . . . . . . . . . . 16 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((v ·Q w) ·Q (*Qw)) Q)
66 recmulnqg 6239 . . . . . . . . . . . . . . . 16 ((((*Q‘(v ·Q w)) ·Q w) Q ((v ·Q w) ·Q (*Qw)) Q) → ((*Q‘((*Q‘(v ·Q w)) ·Q w)) = ((v ·Q w) ·Q (*Qw)) ↔ (((*Q‘(v ·Q w)) ·Q w) ·Q ((v ·Q w) ·Q (*Qw))) = 1Q))
6764, 65, 66syl2anc 391 . . . . . . . . . . . . . . 15 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((*Q‘((*Q‘(v ·Q w)) ·Q w)) = ((v ·Q w) ·Q (*Qw)) ↔ (((*Q‘(v ·Q w)) ·Q w) ·Q ((v ·Q w) ·Q (*Qw))) = 1Q))
6863, 67mpbird 156 . . . . . . . . . . . . . 14 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (*Q‘((*Q‘(v ·Q w)) ·Q w)) = ((v ·Q w) ·Q (*Qw)))
6968eleq1d 2082 . . . . . . . . . . . . 13 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((*Q‘((*Q‘(v ·Q w)) ·Q w)) (1stA) ↔ ((v ·Q w) ·Q (*Qw)) (1stA)))
7069biimprd 147 . . . . . . . . . . . 12 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (((v ·Q w) ·Q (*Qw)) (1stA) → (*Q‘((*Q‘(v ·Q w)) ·Q w)) (1stA)))
71 breq1 3733 . . . . . . . . . . . . . . . 16 (y = ((*Q‘(v ·Q w)) ·Q w) → (y <Q ((*Qz) ·Q w) ↔ ((*Q‘(v ·Q w)) ·Q w) <Q ((*Qz) ·Q w)))
72 fveq2 5094 . . . . . . . . . . . . . . . . 17 (y = ((*Q‘(v ·Q w)) ·Q w) → (*Qy) = (*Q‘((*Q‘(v ·Q w)) ·Q w)))
7372eleq1d 2082 . . . . . . . . . . . . . . . 16 (y = ((*Q‘(v ·Q w)) ·Q w) → ((*Qy) (1stA) ↔ (*Q‘((*Q‘(v ·Q w)) ·Q w)) (1stA)))
7471, 73anbi12d 442 . . . . . . . . . . . . . . 15 (y = ((*Q‘(v ·Q w)) ·Q w) → ((y <Q ((*Qz) ·Q w) (*Qy) (1stA)) ↔ (((*Q‘(v ·Q w)) ·Q w) <Q ((*Qz) ·Q w) (*Q‘((*Q‘(v ·Q w)) ·Q w)) (1stA))))
7574spcegv 2612 . . . . . . . . . . . . . 14 (((*Q‘(v ·Q w)) ·Q w) Q → ((((*Q‘(v ·Q w)) ·Q w) <Q ((*Qz) ·Q w) (*Q‘((*Q‘(v ·Q w)) ·Q w)) (1stA)) → y(y <Q ((*Qz) ·Q w) (*Qy) (1stA))))
7664, 75syl 14 . . . . . . . . . . . . 13 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((((*Q‘(v ·Q w)) ·Q w) <Q ((*Qz) ·Q w) (*Q‘((*Q‘(v ·Q w)) ·Q w)) (1stA)) → y(y <Q ((*Qz) ·Q w) (*Qy) (1stA))))
77 recexpr.1 . . . . . . . . . . . . . 14 B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩
7877recexprlemelu 6447 . . . . . . . . . . . . 13 (((*Qz) ·Q w) (2ndB) ↔ y(y <Q ((*Qz) ·Q w) (*Qy) (1stA)))
7976, 78syl6ibr 151 . . . . . . . . . . . 12 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((((*Q‘(v ·Q w)) ·Q w) <Q ((*Qz) ·Q w) (*Q‘((*Q‘(v ·Q w)) ·Q w)) (1stA)) → ((*Qz) ·Q w) (2ndB)))
8047, 70, 79syl2and 279 . . . . . . . . . . 11 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((z <Q (v ·Q w) ((v ·Q w) ·Q (*Qw)) (1stA)) → ((*Qz) ·Q w) (2ndB)))
819, 31, 80mp2and 409 . . . . . . . . . 10 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((*Qz) ·Q w) (2ndB))
82 mulidnq 6237 . . . . . . . . . . . . . 14 (w Q → (w ·Q 1Q) = w)
83 mulcomnqg 6231 . . . . . . . . . . . . . . 15 ((w Q 1Q Q) → (w ·Q 1Q) = (1Q ·Q w))
8448, 83mpan2 401 . . . . . . . . . . . . . 14 (w Q → (w ·Q 1Q) = (1Q ·Q w))
8582, 84eqtr3d 2050 . . . . . . . . . . . . 13 (w Qw = (1Q ·Q w))
8685adantl 262 . . . . . . . . . . . 12 ((z Q w Q) → w = (1Q ·Q w))
87 recidnq 6241 . . . . . . . . . . . . . 14 (z Q → (z ·Q (*Qz)) = 1Q)
8887oveq1d 5442 . . . . . . . . . . . . 13 (z Q → ((z ·Q (*Qz)) ·Q w) = (1Q ·Q w))
8988adantr 261 . . . . . . . . . . . 12 ((z Q w Q) → ((z ·Q (*Qz)) ·Q w) = (1Q ·Q w))
90 mulassnqg 6232 . . . . . . . . . . . . . 14 ((z Q (*Qz) Q w Q) → ((z ·Q (*Qz)) ·Q w) = (z ·Q ((*Qz) ·Q w)))
9142, 90syl3an2 1152 . . . . . . . . . . . . 13 ((z Q z Q w Q) → ((z ·Q (*Qz)) ·Q w) = (z ·Q ((*Qz) ·Q w)))
92913anidm12 1175 . . . . . . . . . . . 12 ((z Q w Q) → ((z ·Q (*Qz)) ·Q w) = (z ·Q ((*Qz) ·Q w)))
9386, 89, 923eqtr2d 2054 . . . . . . . . . . 11 ((z Q w Q) → w = (z ·Q ((*Qz) ·Q w)))
9441, 19, 93syl2anc 391 . . . . . . . . . 10 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → w = (z ·Q ((*Qz) ·Q w)))
95 oveq2 5435 . . . . . . . . . . . 12 (x = ((*Qz) ·Q w) → (z ·Q x) = (z ·Q ((*Qz) ·Q w)))
9695eqeq2d 2027 . . . . . . . . . . 11 (x = ((*Qz) ·Q w) → (w = (z ·Q x) ↔ w = (z ·Q ((*Qz) ·Q w))))
9796rspcev 2627 . . . . . . . . . 10 ((((*Qz) ·Q w) (2ndB) w = (z ·Q ((*Qz) ·Q w))) → x (2ndB)w = (z ·Q x))
9881, 94, 97syl2anc 391 . . . . . . . . 9 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → x (2ndB)w = (z ·Q x))
99983expia 1089 . . . . . . . 8 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA))) → (z <Q (v ·Q w) → x (2ndB)w = (z ·Q x)))
10099reximdv 2392 . . . . . . 7 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA))) → (z (2ndA)z <Q (v ·Q w) → z (2ndA)x (2ndB)w = (z ·Q x)))
10177recexprlempr 6456 . . . . . . . . 9 (A PB P)
102 df-imp 6312 . . . . . . . . . 10 ·P = (y P, w P ↦ ⟨{u Qf Q g Q (f (1sty) g (1stw) u = (f ·Q g))}, {u Qf Q g Q (f (2ndy) g (2ndw) u = (f ·Q g))}⟩)
103102, 59genpelvu 6356 . . . . . . . . 9 ((A P B P) → (w (2nd ‘(A ·P B)) ↔ z (2ndA)x (2ndB)w = (z ·Q x)))
104101, 103mpdan 398 . . . . . . . 8 (A P → (w (2nd ‘(A ·P B)) ↔ z (2ndA)x (2ndB)w = (z ·Q x)))
105104ad2antrr 457 . . . . . . 7 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA))) → (w (2nd ‘(A ·P B)) ↔ z (2ndA)x (2ndB)w = (z ·Q x)))
106100, 105sylibrd 158 . . . . . 6 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA))) → (z (2ndA)z <Q (v ·Q w) → w (2nd ‘(A ·P B))))
1078, 106mpd 13 . . . . 5 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA))) → w (2nd ‘(A ·P B)))
1085, 107rexlimddv 2409 . . . 4 ((A P 1Q <Q w) → w (2nd ‘(A ·P B)))
109108ex 108 . . 3 (A P → (1Q <Q ww (2nd ‘(A ·P B))))
1102, 109syl5bi 141 . 2 (A P → (w (2nd ‘1P) → w (2nd ‘(A ·P B))))
111110ssrdv 2922 1 (A P → (2nd ‘1P) ⊆ (2nd ‘(A ·P B)))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   w3a 869   = wceq 1226  wex 1357   wcel 1369  {cab 2002  wrex 2279  wss 2888  cop 3345   class class class wbr 3730  cfv 4820  (class class class)co 5427  1st c1st 5679  2nd c2nd 5680  Qcnq 6129  1Qc1q 6130   ·Q cmq 6132  *Qcrq 6133   <Q cltq 6134  Pcnp 6140  1Pc1p 6141   ·P cmp 6143
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 529  ax-in2 530  ax-io 614  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1358  ax-ie2 1359  ax-8 1371  ax-10 1372  ax-11 1373  ax-i12 1374  ax-bnd 1375  ax-4 1376  ax-13 1380  ax-14 1381  ax-17 1395  ax-i9 1399  ax-ial 1403  ax-i5r 1404  ax-ext 1998  ax-coll 3838  ax-sep 3841  ax-nul 3849  ax-pow 3893  ax-pr 3910  ax-un 4111  ax-setind 4195  ax-iinf 4229
This theorem depends on definitions:  df-bi 110  df-dc 727  df-3or 870  df-3an 871  df-tru 1229  df-fal 1232  df-nf 1326  df-sb 1622  df-eu 1879  df-mo 1880  df-clab 2003  df-cleq 2009  df-clel 2012  df-nfc 2143  df-ne 2182  df-ral 2283  df-rex 2284  df-reu 2285  df-rab 2287  df-v 2531  df-sbc 2736  df-csb 2824  df-dif 2891  df-un 2893  df-in 2895  df-ss 2902  df-nul 3196  df-pw 3328  df-sn 3348  df-pr 3349  df-op 3351  df-uni 3547  df-int 3582  df-iun 3625  df-br 3731  df-opab 3785  df-mpt 3786  df-tr 3821  df-eprel 3992  df-id 3996  df-po 3999  df-iso 4000  df-iord 4044  df-on 4046  df-suc 4049  df-iom 4232  df-xp 4269  df-rel 4270  df-cnv 4271  df-co 4272  df-dm 4273  df-rn 4274  df-res 4275  df-ima 4276  df-iota 4785  df-fun 4822  df-fn 4823  df-f 4824  df-f1 4825  df-fo 4826  df-f1o 4827  df-fv 4828  df-ov 5430  df-oprab 5431  df-mpt2 5432  df-1st 5681  df-2nd 5682  df-recs 5833  df-irdg 5869  df-1o 5907  df-2o 5908  df-oadd 5911  df-omul 5912  df-er 6008  df-ec 6010  df-qs 6014  df-ni 6153  df-pli 6154  df-mi 6155  df-lti 6156  df-plpq 6192  df-mpq 6193  df-enq 6195  df-nqqs 6196  df-plqqs 6197  df-mqqs 6198  df-1nqqs 6199  df-rq 6200  df-ltnqqs 6201  df-enq0 6268  df-nq0 6269  df-0nq0 6270  df-plq0 6271  df-mq0 6272  df-inp 6309  df-i1p 6310  df-imp 6312
This theorem is referenced by:  recexprlemex  6461
  Copyright terms: Public domain W3C validator