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

Theorem wefrc 3678
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 3671 . . 3 |- (B C_ A -> ( _E We A -> _E We B))
2 n0 2915 . . . 4 |- (B =/= (/) <-> E.y y e. B)
3 ineq2 2824 . . . . . . . . . . 11 |- (x = y -> (B i^i x) = (B i^i y))
43eqeq1d 1946 . . . . . . . . . 10 |- (x = y -> ((B i^i x) = (/) <-> (B i^i y) = (/)))
54rcla4ev 2429 . . . . . . . . 9 |- ((y e. B /\ (B i^i y) = (/)) -> E.x e. B (B i^i x) = (/))
65ex 426 . . . . . . . 8 |- (y e. B -> ((B i^i y) = (/) -> E.x e. B (B i^i x) = (/)))
76adantl 453 . . . . . . 7 |- (( _E We B /\ y e. B) -> ((B i^i y) = (/) -> E.x e. B (B i^i x) = (/)))
8 inss1 2847 . . . . . . . . . . 11 |- (B i^i y) C_ B
9 wefr 3674 . . . . . . . . . . . . 13 |- ( _E We B -> _E Fr B)
10 vex 2346 . . . . . . . . . . . . . . 15 |- y e. _V
1110inex2 3475 . . . . . . . . . . . . . 14 |- (B i^i y) e. _V
1211epfrc 3669 . . . . . . . . . . . . 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 1195 . . . . . . . . . . . 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 1131 . . . . . . . . . . 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 2820 . . . . . . . . . . . . 13 |- (x e. (B i^i y) <-> (x e. B /\ x e. y))
1716anbi1i 681 . . . . . . . . . . . 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 633 . . . . . . . . . . . 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 239 . . . . . . . . . . 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 2174 . . . . . . . . . 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 216 . . . . . . . . 9 |- ( _E We B -> ((B i^i y) =/= (/) -> E.x e. B (x e. y /\ ((B i^i y) i^i x) = (/))))
2221adantr 452 . . . . . . . 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 2820 . . . . . . . . . . . . . . . . 17 |- (z e. (B i^i x) <-> (z e. B /\ z e. x))
24 df-3an 923 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((y e. B /\ z e. B /\ x e. B) <-> ((y e. B /\ z e. B) /\ x e. B))
25 3anrot 926 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((y e. B /\ z e. B /\ x e. B) <-> (z e. B /\ x e. B /\ y e. B))
2624, 25bitr3i 241 . . . . . . . . . . . . . . . . . . . . . 22 |- (((y e. B /\ z e. B) /\ x e. B) <-> (z e. B /\ x e. B /\ y e. B))
27 wetrep 3677 . . . . . . . . . . . . . . . . . . . . . . 23 |- (( _E We B /\ (z e. B /\ x e. B /\ y e. B)) -> ((z e. x /\ x e. y) -> z e. y))
2827exp3a 428 . . . . . . . . . . . . . . . . . . . . . 22 |- (( _E We B /\ (z e. B /\ x e. B /\ y e. B)) -> (z e. x -> (x e. y -> z e. y)))
2926, 28sylan2b 462 . . . . . . . . . . . . . . . . . . . . 21 |- (( _E We B /\ ((y e. B /\ z e. B) /\ x e. B)) -> (z e. x -> (x e. y -> z e. y)))
3029exp44 598 . . . . . . . . . . . . . . . . . . . 20 |- ( _E We B -> (y e. B -> (z e. B -> (x e. B -> (z e. x -> (x e. y -> z e. y))))))
3130imp 421 . . . . . . . . . . . . . . . . . . 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 423 . . . . . . . . . . . . . . . . 17 |- (( _E We B /\ y e. B) -> ((z e. B /\ z e. x) -> (x e. B -> (x e. y -> z e. y))))
3423, 33syl5bi 206 . . . . . . . . . . . . . . . 16 |- (( _E We B /\ y e. B) -> (z e. (B i^i x) -> (x e. B -> (x e. y -> z e. y))))
3534imp4a 574 . . . . . . . . . . . . . . 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 2226 . . . . . . . . . . . . 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 2657 . . . . . . . . . . . . 13 |- ((B i^i x) C_ y <-> A.z e. (B i^i x)z e. y)
3937, 38syl6ibr 217 . . . . . . . . . . . 12 |- (( _E We B /\ y e. B) -> ((x e. B /\ x e. y) -> (B i^i x) C_ y))
40 dfss 2652 . . . . . . . . . . . . . . . 16 |- ((B i^i x) C_ y <-> (B i^i x) = ((B i^i x) i^i y))
41 in32 2839 . . . . . . . . . . . . . . . . 17 |- ((B i^i x) i^i y) = ((B i^i y) i^i x)
4241eqeq2i 1948 . . . . . . . . . . . . . . . 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 239 . . . . . . . . . . . . . . 15 |- ((B i^i x) C_ y <-> (B i^i x) = ((B i^i y) i^i x))
4443biimpi 184 . . . . . . . . . . . . . 14 |- ((B i^i x) C_ y -> (B i^i x) = ((B i^i y) i^i x))
4544eqeq1d 1946 . . . . . . . . . . . . 13 |- ((B i^i x) C_ y -> ((B i^i x) = (/) <-> ((B i^i y) i^i x) = (/)))
4645biimprd 212 . . . . . . . . . . . 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 428 . . . . . . . . . 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 574 . . . . . . . . 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 2247 . . . . . . . 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 2129 . . . . . 6 |- (( _E We B /\ y e. B) -> E.x e. B (B i^i x) = (/))
5352ex 426 . . . . 5 |- ( _E We B -> (y e. B -> E.x e. B (B i^i x) = (/)))
5453exlimdv 1655 . . . 4 |- ( _E We B -> (E.y y e. B -> E.x e. B (B i^i x) = (/)))
552, 54syl5bi 206 . . 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 1126 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 361   /\ w3a 921  E.wex 1355   = wceq 1434   e. wcel 1436   =/= wne 2056  A.wral 2147  E.wrex 2148   i^i cin 2641   C_ wss 2642  (/)c0 2906   _E cep 3611   Fr wfr 3652   We wwe 3653
This theorem is referenced by:  tz7.5 3704  finminlem 16869
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1351  ax-6 1352  ax-7 1353  ax-gen 1354  ax-8 1438  ax-10 1439  ax-11 1440  ax-12 1441  ax-14 1443  ax-17 1450  ax-9 1465  ax-4 1471  ax-16 1649  ax-ext 1920  ax-sep 3459  ax-nul 3468  ax-pr 3528
This theorem depends on definitions:  df-bi 175  df-or 362  df-an 363  df-3an 923  df-ex 1356  df-sb 1611  df-eu 1838  df-mo 1839  df-clab 1926  df-cleq 1931  df-clel 1934  df-ne 2058  df-ral 2151  df-rex 2152  df-v 2345  df-dif 2645  df-un 2647  df-in 2649  df-ss 2651  df-nul 2907  df-sn 3085  df-pr 3086  df-op 3088  df-br 3364  df-opab 3418  df-eprel 3613  df-po 3621  df-so 3635  df-fr 3654  df-we 3670
Copyright terms: Public domain