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

Theorem wefrc 3689
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 3682 . . 3 |- (B C_ A -> ( _E We A -> _E We B))
2 n0 2935 . . . 4 |- (B =/= (/) <-> E.y y e. B)
3 ineq2 2844 . . . . . . . . . . 11 |- (x = y -> (B i^i x) = (B i^i y))
43eqeq1d 1968 . . . . . . . . . 10 |- (x = y -> ((B i^i x) = (/) <-> (B i^i y) = (/)))
54rcla4ev 2451 . . . . . . . . 9 |- ((y e. B /\ (B i^i y) = (/)) -> E.x e. B (B i^i x) = (/))
65ex 448 . . . . . . . 8 |- (y e. B -> ((B i^i y) = (/) -> E.x e. B (B i^i x) = (/)))
76adantl 475 . . . . . . 7 |- (( _E We B /\ y e. B) -> ((B i^i y) = (/) -> E.x e. B (B i^i x) = (/)))
8 inss1 2867 . . . . . . . . . . 11 |- (B i^i y) C_ B
9 wefr 3685 . . . . . . . . . . . . 13 |- ( _E We B -> _E Fr B)
10 vex 2368 . . . . . . . . . . . . . . 15 |- y e. _V
1110inex2 3488 . . . . . . . . . . . . . 14 |- (B i^i y) e. _V
1211epfrc 3680 . . . . . . . . . . . . 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 1220 . . . . . . . . . . . 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 1156 . . . . . . . . . . 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 2840 . . . . . . . . . . . . 13 |- (x e. (B i^i y) <-> (x e. B /\ x e. y))
1716anbi1i 704 . . . . . . . . . . . 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 656 . . . . . . . . . . . 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 259 . . . . . . . . . . 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 2196 . . . . . . . . . 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 236 . . . . . . . . 9 |- ( _E We B -> ((B i^i y) =/= (/) -> E.x e. B (x e. y /\ ((B i^i y) i^i x) = (/))))
2221adantr 474 . . . . . . . 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 2840 . . . . . . . . . . . . . . . . 17 |- (z e. (B i^i x) <-> (z e. B /\ z e. x))
24 df-3an 948 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((y e. B /\ z e. B /\ x e. B) <-> ((y e. B /\ z e. B) /\ x e. B))
25 3anrot 951 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((y e. B /\ z e. B /\ x e. B) <-> (z e. B /\ x e. B /\ y e. B))
2624, 25bitr3i 261 . . . . . . . . . . . . . . . . . . . . . 22 |- (((y e. B /\ z e. B) /\ x e. B) <-> (z e. B /\ x e. B /\ y e. B))
27 wetrep 3688 . . . . . . . . . . . . . . . . . . . . . . 23 |- (( _E We B /\ (z e. B /\ x e. B /\ y e. B)) -> ((z e. x /\ x e. y) -> z e. y))
2827exp3a 450 . . . . . . . . . . . . . . . . . . . . . 22 |- (( _E We B /\ (z e. B /\ x e. B /\ y e. B)) -> (z e. x -> (x e. y -> z e. y)))
2926, 28sylan2b 484 . . . . . . . . . . . . . . . . . . . . 21 |- (( _E We B /\ ((y e. B /\ z e. B) /\ x e. B)) -> (z e. x -> (x e. y -> z e. y)))
3029exp44 621 . . . . . . . . . . . . . . . . . . . 20 |- ( _E We B -> (y e. B -> (z e. B -> (x e. B -> (z e. x -> (x e. y -> z e. y))))))
3130imp 443 . . . . . . . . . . . . . . . . . . 19 |- (( _E We B /\ y e. B) -> (z e. B -> (x e. B -> (z e. x -> (x e. y -> z e. y)))))
3231com34 79 . . . . . . . . . . . . . . . . . 18 |- (( _E We B /\ y e. B) -> (z e. B -> (z e. x -> (x e. B -> (x e. y -> z e. y)))))
3332imp3a 445 . . . . . . . . . . . . . . . . 17 |- (( _E We B /\ y e. B) -> ((z e. B /\ z e. x) -> (x e. B -> (x e. y -> z e. y))))
3423, 33syl5bi 226 . . . . . . . . . . . . . . . 16 |- (( _E We B /\ y e. B) -> (z e. (B i^i x) -> (x e. B -> (x e. y -> z e. y))))
3534imp4a 597 . . . . . . . . . . . . . . 15 |- (( _E We B /\ y e. B) -> (z e. (B i^i x) -> ((x e. B /\ x e. y) -> z e. y)))
3635com23 74 . . . . . . . . . . . . . 14 |- (( _E We B /\ y e. B) -> ((x e. B /\ x e. y) -> (z e. (B i^i x) -> z e. y)))
3736ralrimdv 2248 . . . . . . . . . . . . 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 2677 . . . . . . . . . . . . 13 |- ((B i^i x) C_ y <-> A.z e. (B i^i x)z e. y)
3937, 38syl6ibr 237 . . . . . . . . . . . 12 |- (( _E We B /\ y e. B) -> ((x e. B /\ x e. y) -> (B i^i x) C_ y))
40 dfss 2672 . . . . . . . . . . . . . . . 16 |- ((B i^i x) C_ y <-> (B i^i x) = ((B i^i x) i^i y))
41 in32 2859 . . . . . . . . . . . . . . . . 17 |- ((B i^i x) i^i y) = ((B i^i y) i^i x)
4241eqeq2i 1970 . . . . . . . . . . . . . . . 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 259 . . . . . . . . . . . . . . 15 |- ((B i^i x) C_ y <-> (B i^i x) = ((B i^i y) i^i x))
4443biimpi 199 . . . . . . . . . . . . . 14 |- ((B i^i x) C_ y -> (B i^i x) = ((B i^i y) i^i x))
4544eqeq1d 1968 . . . . . . . . . . . . 13 |- ((B i^i x) C_ y -> ((B i^i x) = (/) <-> ((B i^i y) i^i x) = (/)))
4645biimprd 232 . . . . . . . . . . . 12 |- ((B i^i x) C_ y -> (((B i^i y) i^i x) = (/) -> (B i^i x) = (/)))
4739, 46syl6 30 . . . . . . . . . . 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 450 . . . . . . . . . 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 597 . . . . . . . . 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 2269 . . . . . . . 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 41 . . . . . . 7 |- (( _E We B /\ y e. B) -> ((B i^i y) =/= (/) -> E.x e. B (B i^i x) = (/)))
527, 51pm2.61dne 2151 . . . . . 6 |- (( _E We B /\ y e. B) -> E.x e. B (B i^i x) = (/))
5352ex 448 . . . . 5 |- ( _E We B -> (y e. B -> E.x e. B (B i^i x) = (/)))
5453exlimdv 1677 . . . 4 |- ( _E We B -> (E.y y e. B -> E.x e. B (B i^i x) = (/)))
552, 54syl5bi 226 . . 3 |- ( _E We B -> (B =/= (/) -> E.x e. B (B i^i x) = (/)))
561, 55syl6com 32 . 2 |- ( _E We A -> (B C_ A -> (B =/= (/) -> E.x e. B (B i^i x) = (/))))
57563imp 1151 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 382   /\ w3a 946  E.wex 1380   = wceq 1457   e. wcel 1459   =/= wne 2078  A.wral 2169  E.wrex 2170   i^i cin 2661   C_ wss 2662  (/)c0 2926   _E cep 3622   Fr wfr 3663   We wwe 3664
This theorem is referenced by:  tz7.5 3715  finminlem 16099
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1376  ax-6 1377  ax-7 1378  ax-gen 1379  ax-8 1461  ax-10 1462  ax-11 1463  ax-12 1464  ax-14 1466  ax-17 1473  ax-9 1488  ax-4 1494  ax-16 1671  ax-ext 1942  ax-sep 3472  ax-nul 3481  ax-pr 3541
This theorem depends on definitions:  df-bi 190  df-or 383  df-an 384  df-3an 948  df-ex 1381  df-sb 1633  df-eu 1860  df-mo 1861  df-clab 1948  df-cleq 1953  df-clel 1956  df-ne 2080  df-ral 2173  df-rex 2174  df-v 2367  df-dif 2665  df-un 2667  df-in 2669  df-ss 2671  df-nul 2927  df-sn 3099  df-pr 3100  df-op 3103  df-br 3377  df-opab 3431  df-eprel 3624  df-po 3632  df-so 3646  df-fr 3665  df-we 3681
Copyright terms: Public domain