HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem wefrc 3686
Description: A non-empty (possibly proper) subclass of a class well-ordered by _E has a minimal element. Special case of Proposition 6.26 of [TakeutiZaring] p. 31.
Assertion
Ref Expression
wefrc |- (( _E We A /\ B C_ A /\ B =/= (/)) -> E.x e. B (B i^i x) = (/))
Distinct variable group:   x,B
Allowed substitution hint:   A(x)

Proof of Theorem wefrc
StepHypRef Expression
1 wess 3679 . . 3 |- (B C_ A -> ( _E We A -> _E We B))
2 n0 2930 . . . 4 |- (B =/= (/) <-> E.y y e. B)
3 ineq2 2839 . . . . . . . . . . 11 |- (x = y -> (B i^i x) = (B i^i y))
43eqeq1d 1961 . . . . . . . . . 10 |- (x = y -> ((B i^i x) = (/) <-> (B i^i y) = (/)))
54rcla4ev 2444 . . . . . . . . 9 |- ((y e. B /\ (B i^i y) = (/)) -> E.x e. B (B i^i x) = (/))
65ex 442 . . . . . . . 8 |- (y e. B -> ((B i^i y) = (/) -> E.x e. B (B i^i x) = (/)))
76adantl 469 . . . . . . 7 |- (( _E We B /\ y e. B) -> ((B i^i y) = (/) -> E.x e. B (B i^i x) = (/)))
8 inss1 2862 . . . . . . . . . . 11 |- (B i^i y) C_ B
9 wefr 3682 . . . . . . . . . . . . 13 |- ( _E We B -> _E Fr B)
10 vex 2361 . . . . . . . . . . . . . . 15 |- y e. _V
1110inex2 3485 . . . . . . . . . . . . . 14 |- (B i^i y) e. _V
1211epfrc 3677 . . . . . . . . . . . . 13 |- (( _E Fr B /\ (B i^i y) C_ B /\ (B i^i y) =/= (/)) -> E.x e. (B i^i y)((B i^i y) i^i x) = (/))
139, 12syl3an1 1211 . . . . . . . . . . . 12 |- (( _E We B /\ (B i^i y) C_ B /\ (B i^i y) =/= (/)) -> E.x e. (B i^i y)((B i^i y) i^i x) = (/))
14133exp 1147 . . . . . . . . . . 11 |- ( _E We B -> ((B i^i y) C_ B -> ((B i^i y) =/= (/) -> E.x e. (B i^i y)((B i^i y) i^i x) = (/))))
158, 14mpi 15 . . . . . . . . . 10 |- ( _E We B -> ((B i^i y) =/= (/) -> E.x e. (B i^i y)((B i^i y) i^i x) = (/)))
16 elin 2835 . . . . . . . . . . . . 13 |- (x e. (B i^i y) <-> (x e. B /\ x e. y))
1716anbi1i 695 . . . . . . . . . . . 12 |- ((x e. (B i^i y) /\ ((B i^i y) i^i x) = (/)) <-> ((x e. B /\ x e. y) /\ ((B i^i y) i^i x) = (/)))
18 anass 647 . . . . . . . . . . . 12 |- (((x e. B /\ x e. y) /\ ((B i^i y) i^i x) = (/)) <-> (x e. B /\ (x e. y /\ ((B i^i y) i^i x) = (/))))
1917, 18bitri 254 . . . . . . . . . . 11 |- ((x e. (B i^i y) /\ ((B i^i y) i^i x) = (/)) <-> (x e. B /\ (x e. y /\ ((B i^i y) i^i x) = (/))))
2019rexbii2 2189 . . . . . . . . . 10 |- (E.x e. (B i^i y)((B i^i y) i^i x) = (/) <-> E.x e. B (x e. y /\ ((B i^i y) i^i x) = (/)))
2115, 20syl6ib 231 . . . . . . . . 9 |- ( _E We B -> ((B i^i y) =/= (/) -> E.x e. B (x e. y /\ ((B i^i y) i^i x) = (/))))
2221adantr 468 . . . . . . . 8 |- (( _E We B /\ y e. B) -> ((B i^i y) =/= (/) -> E.x e. B (x e. y /\ ((B i^i y) i^i x) = (/))))
23 elin 2835 . . . . . . . . . . . . . . . . 17 |- (z e. (B i^i x) <-> (z e. B /\ z e. x))
24 df-3an 939 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((y e. B /\ z e. B /\ x e. B) <-> ((y e. B /\ z e. B) /\ x e. B))
25 3anrot 942 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((y e. B /\ z e. B /\ x e. B) <-> (z e. B /\ x e. B /\ y e. B))
2624, 25bitr3i 256 . . . . . . . . . . . . . . . . . . . . . 22 |- (((y e. B /\ z e. B) /\ x e. B) <-> (z e. B /\ x e. B /\ y e. B))
27 wetrep 3685 . . . . . . . . . . . . . . . . . . . . . . 23 |- (( _E We B /\ (z e. B /\ x e. B /\ y e. B)) -> ((z e. x /\ x e. y) -> z e. y))
2827exp3a 444 . . . . . . . . . . . . . . . . . . . . . 22 |- (( _E We B /\ (z e. B /\ x e. B /\ y e. B)) -> (z e. x -> (x e. y -> z e. y)))
2926, 28sylan2b 478 . . . . . . . . . . . . . . . . . . . . 21 |- (( _E We B /\ ((y e. B /\ z e. B) /\ x e. B)) -> (z e. x -> (x e. y -> z e. y)))
3029exp44 612 . . . . . . . . . . . . . . . . . . . 20 |- ( _E We B -> (y e. B -> (z e. B -> (x e. B -> (z e. x -> (x e. y -> z e. y))))))
3130imp 437 . . . . . . . . . . . . . . . . . . 19 |- (( _E We B /\ y e. B) -> (z e. B -> (x e. B -> (z e. x -> (x e. y -> z e. y)))))
3231com34 76 . . . . . . . . . . . . . . . . . 18 |- (( _E We B /\ y e. B) -> (z e. B -> (z e. x -> (x e. B -> (x e. y -> z e. y)))))
3332imp3a 439 . . . . . . . . . . . . . . . . 17 |- (( _E We B /\ y e. B) -> ((z e. B /\ z e. x) -> (x e. B -> (x e. y -> z e. y))))
3423, 33syl5bi 221 . . . . . . . . . . . . . . . 16 |- (( _E We B /\ y e. B) -> (z e. (B i^i x) -> (x e. B -> (x e. y -> z e. y))))
3534imp4a 588 . . . . . . . . . . . . . . 15 |- (( _E We B /\ y e. B) -> (z e. (B i^i x) -> ((x e. B /\ x e. y) -> z e. y)))
3635com23 71 . . . . . . . . . . . . . 14 |- (( _E We B /\ y e. B) -> ((x e. B /\ x e. y) -> (z e. (B i^i x) -> z e. y)))
3736ralrimdv 2241 . . . . . . . . . . . . 13 |- (( _E We B /\ y e. B) -> ((x e. B /\ x e. y) -> A.z e. (B i^i x)z e. y))
38 dfss3 2672 . . . . . . . . . . . . 13 |- ((B i^i x) C_ y <-> A.z e. (B i^i x)z e. y)
3937, 38syl6ibr 232 . . . . . . . . . . . 12 |- (( _E We B /\ y e. B) -> ((x e. B /\ x e. y) -> (B i^i x) C_ y))
40 dfss 2667 . . . . . . . . . . . . . . . 16 |- ((B i^i x) C_ y <-> (B i^i x) = ((B i^i x) i^i y))
41 in32 2854 . . . . . . . . . . . . . . . . 17 |- ((B i^i x) i^i y) = ((B i^i y) i^i x)
4241eqeq2i 1963 . . . . . . . . . . . . . . . 16 |- ((B i^i x) = ((B i^i x) i^i y) <-> (B i^i x) = ((B i^i y) i^i x))
4340, 42bitri 254 . . . . . . . . . . . . . . 15 |- ((B i^i x) C_ y <-> (B i^i x) = ((B i^i y) i^i x))
4443biimpi 194 . . . . . . . . . . . . . 14 |- ((B i^i x) C_ y -> (B i^i x) = ((B i^i y) i^i x))
4544eqeq1d 1961 . . . . . . . . . . . . 13 |- ((B i^i x) C_ y -> ((B i^i x) = (/) <-> ((B i^i y) i^i x) = (/)))
4645biimprd 227 . . . . . . . . . . . 12 |- ((B i^i x) C_ y -> (((B i^i y) i^i x) = (/) -> (B i^i x) = (/)))
4739, 46syl6 28 . . . . . . . . . . 11 |- (( _E We B /\ y e. B) -> ((x e. B /\ x e. y) -> (((B i^i y) i^i x) = (/) -> (B i^i x) = (/))))
4847exp3a 444 . . . . . . . . . 10 |- (( _E We B /\ y e. B) -> (x e. B -> (x e. y -> (((B i^i y) i^i x) = (/) -> (B i^i x) = (/)))))
4948imp4a 588 . . . . . . . . 9 |- (( _E We B /\ y e. B) -> (x e. B -> ((x e. y /\ ((B i^i y) i^i x) = (/)) -> (B i^i x) = (/))))
5049reximdvai 2262 . . . . . . . 8 |- (( _E We B /\ y e. B) -> (E.x e. B (x e. y /\ ((B i^i y) i^i x) = (/)) -> E.x e. B (B i^i x) = (/)))
5122, 50syld 39 . . . . . . 7 |- (( _E We B /\ y e. B) -> ((B i^i y) =/= (/) -> E.x e. B (B i^i x) = (/)))
527, 51pm2.61dne 2144 . . . . . 6 |- (( _E We B /\ y e. B) -> E.x e. B (B i^i x) = (/))
5352ex 442 . . . . 5 |- ( _E We B -> (y e. B -> E.x e. B (B i^i x) = (/)))
5453exlimdv 1670 . . . 4 |- ( _E We B -> (E.y y e. B -> E.x e. B (B i^i x) = (/)))
552, 54syl5bi 221 . . 3 |- ( _E We B -> (B =/= (/) -> E.x e. B (B i^i x) = (/)))
561, 55syl6com 30 . 2 |- ( _E We A -> (B C_ A -> (B =/= (/) -> E.x e. B (B i^i x) = (/))))
57563imp 1142 1 |- (( _E We A /\ B C_ A /\ B =/= (/)) -> E.x e. B (B i^i x) = (/))
Colors of variables: wff set class
Syntax hints:   -> wi 4   /\ wa 377   /\ w3a 937  E.wex 1371   = wceq 1449   e. wcel 1451   =/= wne 2071  A.wral 2162  E.wrex 2163   i^i cin 2656   C_ wss 2657  (/)c0 2921   _E cep 3619   Fr wfr 3660   We wwe 3661
This theorem is referenced by:  tz7.5 3712  finminlem 16691
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1367  ax-6 1368  ax-7 1369  ax-gen 1370  ax-8 1453  ax-10 1454  ax-11 1455  ax-12 1456  ax-14 1458  ax-17 1465  ax-9 1480  ax-4 1486  ax-16 1664  ax-ext 1935  ax-sep 3469  ax-nul 3478  ax-pr 3538
This theorem depends on definitions:  df-bi 185  df-or 378  df-an 379  df-3an 939  df-ex 1372  df-sb 1626  df-eu 1853  df-mo 1854  df-clab 1941  df-cleq 1946  df-clel 1949  df-ne 2073  df-ral 2166  df-rex 2167  df-v 2360  df-dif 2660  df-un 2662  df-in 2664  df-ss 2666  df-nul 2922  df-sn 3096  df-pr 3097  df-op 3100  df-br 3374  df-opab 3428  df-eprel 3621  df-po 3629  df-so 3643  df-fr 3662  df-we 3678
Copyright terms: Public domain