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

Theorem wefrc 3669
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 3662 . . 3 |- (B C_ A -> ( _E We A -> _E We B))
2 n0 2909 . . . 4 |- (B =/= (/) <-> E.y y e. B)
3 ineq2 2818 . . . . . . . . . . 11 |- (x = y -> (B i^i x) = (B i^i y))
43eqeq1d 1940 . . . . . . . . . 10 |- (x = y -> ((B i^i x) = (/) <-> (B i^i y) = (/)))
54rcla4ev 2423 . . . . . . . . 9 |- ((y e. B /\ (B i^i y) = (/)) -> E.x e. B (B i^i x) = (/))
65ex 422 . . . . . . . 8 |- (y e. B -> ((B i^i y) = (/) -> E.x e. B (B i^i x) = (/)))
76adantl 449 . . . . . . 7 |- (( _E We B /\ y e. B) -> ((B i^i y) = (/) -> E.x e. B (B i^i x) = (/)))
8 inss1 2841 . . . . . . . . . . 11 |- (B i^i y) C_ B
9 wefr 3665 . . . . . . . . . . . . 13 |- ( _E We B -> _E Fr B)
10 vex 2340 . . . . . . . . . . . . . . 15 |- y e. _V
1110inex2 3466 . . . . . . . . . . . . . 14 |- (B i^i y) e. _V
1211epfrc 3660 . . . . . . . . . . . . 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 1189 . . . . . . . . . . . 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 1125 . . . . . . . . . . 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 2814 . . . . . . . . . . . . 13 |- (x e. (B i^i y) <-> (x e. B /\ x e. y))
1716anbi1i 675 . . . . . . . . . . . 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 627 . . . . . . . . . . . 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 240 . . . . . . . . . . 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 2168 . . . . . . . . . 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 217 . . . . . . . . 9 |- ( _E We B -> ((B i^i y) =/= (/) -> E.x e. B (x e. y /\ ((B i^i y) i^i x) = (/))))
2221adantr 448 . . . . . . . 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 2814 . . . . . . . . . . . . . . . . 17 |- (z e. (B i^i x) <-> (z e. B /\ z e. x))
24 df-3an 917 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((y e. B /\ z e. B /\ x e. B) <-> ((y e. B /\ z e. B) /\ x e. B))
25 3anrot 920 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((y e. B /\ z e. B /\ x e. B) <-> (z e. B /\ x e. B /\ y e. B))
2624, 25bitr3i 242 . . . . . . . . . . . . . . . . . . . . . 22 |- (((y e. B /\ z e. B) /\ x e. B) <-> (z e. B /\ x e. B /\ y e. B))
27 wetrep 3668 . . . . . . . . . . . . . . . . . . . . . . 23 |- (( _E We B /\ (z e. B /\ x e. B /\ y e. B)) -> ((z e. x /\ x e. y) -> z e. y))
2827exp3a 424 . . . . . . . . . . . . . . . . . . . . . 22 |- (( _E We B /\ (z e. B /\ x e. B /\ y e. B)) -> (z e. x -> (x e. y -> z e. y)))
2926, 28sylan2b 458 . . . . . . . . . . . . . . . . . . . . 21 |- (( _E We B /\ ((y e. B /\ z e. B) /\ x e. B)) -> (z e. x -> (x e. y -> z e. y)))
3029exp44 592 . . . . . . . . . . . . . . . . . . . 20 |- ( _E We B -> (y e. B -> (z e. B -> (x e. B -> (z e. x -> (x e. y -> z e. y))))))
3130imp 417 . . . . . . . . . . . . . . . . . . 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 419 . . . . . . . . . . . . . . . . 17 |- (( _E We B /\ y e. B) -> ((z e. B /\ z e. x) -> (x e. B -> (x e. y -> z e. y))))
3423, 33syl5bi 207 . . . . . . . . . . . . . . . 16 |- (( _E We B /\ y e. B) -> (z e. (B i^i x) -> (x e. B -> (x e. y -> z e. y))))
3534imp4a 568 . . . . . . . . . . . . . . 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 2220 . . . . . . . . . . . . 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 2651 . . . . . . . . . . . . 13 |- ((B i^i x) C_ y <-> A.z e. (B i^i x)z e. y)
3937, 38syl6ibr 218 . . . . . . . . . . . 12 |- (( _E We B /\ y e. B) -> ((x e. B /\ x e. y) -> (B i^i x) C_ y))
40 dfss 2646 . . . . . . . . . . . . . . . 16 |- ((B i^i x) C_ y <-> (B i^i x) = ((B i^i x) i^i y))
41 in32 2833 . . . . . . . . . . . . . . . . 17 |- ((B i^i x) i^i y) = ((B i^i y) i^i x)
4241eqeq2i 1942 . . . . . . . . . . . . . . . 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 240 . . . . . . . . . . . . . . 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 1940 . . . . . . . . . . . . 13 |- ((B i^i x) C_ y -> ((B i^i x) = (/) <-> ((B i^i y) i^i x) = (/)))
4645biimprd 213 . . . . . . . . . . . 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 424 . . . . . . . . . 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 568 . . . . . . . . 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 2241 . . . . . . . 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 2123 . . . . . 6 |- (( _E We B /\ y e. B) -> E.x e. B (B i^i x) = (/))
5352ex 422 . . . . 5 |- ( _E We B -> (y e. B -> E.x e. B (B i^i x) = (/)))
5453exlimdv 1649 . . . 4 |- ( _E We B -> (E.y y e. B -> E.x e. B (B i^i x) = (/)))
552, 54syl5bi 207 . . 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 1120 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 357   /\ w3a 915  E.wex 1349   = wceq 1428   e. wcel 1430   =/= wne 2050  A.wral 2141  E.wrex 2142   i^i cin 2635   C_ wss 2636  (/)c0 2900   _E cep 3602   Fr wfr 3643   We wwe 3644
This theorem is referenced by:  tz7.5 3695  finminlem 16836
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1345  ax-6 1346  ax-7 1347  ax-gen 1348  ax-8 1432  ax-10 1433  ax-11 1434  ax-12 1435  ax-14 1437  ax-17 1444  ax-9 1459  ax-4 1465  ax-16 1643  ax-ext 1914  ax-sep 3450  ax-nul 3459  ax-pr 3519
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 917  df-ex 1350  df-sb 1605  df-eu 1832  df-mo 1833  df-clab 1920  df-cleq 1925  df-clel 1928  df-ne 2052  df-ral 2145  df-rex 2146  df-v 2339  df-dif 2639  df-un 2641  df-in 2643  df-ss 2645  df-nul 2901  df-sn 3077  df-pr 3078  df-op 3080  df-br 3355  df-opab 3409  df-eprel 3604  df-po 3612  df-so 3626  df-fr 3645  df-we 3661
Copyright terms: Public domain