Theorem tz7.7 2224

Description: Proposition 7.7 of [TakeutiZaring] p. 37.

Assertion

Ref	Expression
tz7.7	|- ((Ord A /\ Tr B) -> (B e. A <-> (B (_ A /\ -. B = A)))

Proof of Theorem tz7.7

Step	Hyp	Ref	Expression
1		tz7.2 2183	. . . . 5 |- (((Tr A /\ E Fr A) /\ B e. A) -> (B (_ A /\ -. B = A))
2		ordtr 2213	. . . . . 6 |- (Ord A -> Tr A)
3		ordfr 2214	. . . . . 6 |- (Ord A -> E Fr A)
4	2, 3	jca 236	. . . . 5 |- (Ord A -> (Tr A /\ E Fr A))
5	1, 4	sylan 343	. . . 4 |- ((Ord A /\ B e. A) -> (B (_ A /\ -. B = A))
6	5	exp 291	. . 3 |- (Ord A -> (B e. A -> (B (_ A /\ -. B = A)))
7	6	adantr 306	. 2 |- ((Ord A /\ Tr B) -> (B e. A -> (B (_ A /\ -. B = A)))
8		trss 2050	. . . . . . . . . . . . . . . . . . . 20 |- (Tr A -> (x e. A -> x (_ A))
9		eldifi 1591	. . . . . . . . . . . . . . . . . . . 20 |- (x e. (A \ B) -> x e. A)
10	8, 9	syl5 22	. . . . . . . . . . . . . . . . . . 19 |- (Tr A -> (x e. (A \ B) -> x (_ A))
11		difin0ss 1753	. . . . . . . . . . . . . . . . . . . 20 |- (((A \ B) i^i x) = (/) -> (x (_ A -> x (_ B))
12	11	com12 13	. . . . . . . . . . . . . . . . . . 19 |- (x (_ A -> (((A \ B) i^i x) = (/) -> x (_ B))
13	10, 12	syl6 23	. . . . . . . . . . . . . . . . . 18 |- (Tr A -> (x e. (A \ B) -> (((A \ B) i^i x) = (/) -> x (_ B)))
14	2, 13	syl 12	. . . . . . . . . . . . . . . . 17 |- (Ord A -> (x e. (A \ B) -> (((A \ B) i^i x) = (/) -> x (_ B)))
15	14	ad2antll 320	. . . . . . . . . . . . . . . 16 |- (((Ord A /\ Tr B) /\ B (_ A) -> (x e. (A \ B) -> (((A \ B) i^i x) = (/) -> x (_ B)))
16	15	imp32 281	. . . . . . . . . . . . . . 15 |- ((((Ord A /\ Tr B) /\ B (_ A) /\ (x e. (A \ B) /\ ((A \ B) i^i x) = (/))) -> x (_ B)
17		wecmpep 2193	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((E We A /\ (y e. A /\ x e. A)) -> (y e. x \/ y = x \/ x e. y))
18		ordwe 2212	. . . . . . . . . . . . . . . . . . . . . . 23 |- (Ord A -> E We A)
19		ssel2 1503	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((B (_ A /\ y e. B) -> y e. A)
20	19, 9	anim12i 268	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((B (_ A /\ y e. B) /\ x e. (A \ B)) -> (y e. A /\ x e. A))
21	17, 18, 20	syl2an 349	. . . . . . . . . . . . . . . . . . . . . 22 |- ((Ord A /\ ((B (_ A /\ y e. B) /\ x e. (A \ B))) -> (y e. x \/ y = x \/ x e. y))
22	21	adantlr 310	. . . . . . . . . . . . . . . . . . . . 21 |- (((Ord A /\ Tr B) /\ ((B (_ A /\ y e. B) /\ x e. (A \ B))) -> (y e. x \/ y = x \/ x e. y))
23		eleq1 1149	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y = x -> (y e. B <-> x e. B))
24	23	biimpcd 137	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y e. B -> (y = x -> x e. B))
25		eldifn 1592	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x e. (A \ B) -> -. x e. B)
26	24, 25	nsyli 106	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y e. B -> (x e. (A \ B) -> -. y = x))
27	26	imp 277	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y e. B /\ x e. (A \ B)) -> -. y = x)
28	27	adantll 309	. . . . . . . . . . . . . . . . . . . . . 22 |- (((B (_ A /\ y e. B) /\ x e. (A \ B)) -> -. y = x)
29	28	adantl 305	. . . . . . . . . . . . . . . . . . . . 21 |- (((Ord A /\ Tr B) /\ ((B (_ A /\ y e. B) /\ x e. (A \ B))) -> -. y = x)
30		trel 2048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (Tr B -> ((x e. y /\ y e. B) -> x e. B))
31	30	exp3a 292	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (Tr B -> (x e. y -> (y e. B -> x e. B)))
32	31	com23 32	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (Tr B -> (y e. B -> (x e. y -> x e. B)))
33	32	imp 277	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((Tr B /\ y e. B) -> (x e. y -> x e. B))
34	33, 25	nsyli 106	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((Tr B /\ y e. B) -> (x e. (A \ B) -> -. x e. y))
35	34	exp 291	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (Tr B -> (y e. B -> (x e. (A \ B) -> -. x e. y)))
36	35	adantld 307	. . . . . . . . . . . . . . . . . . . . . . 23 |- (Tr B -> ((B (_ A /\ y e. B) -> (x e. (A \ B) -> -. x e. y)))
37	36	imp32 281	. . . . . . . . . . . . . . . . . . . . . 22 |- ((Tr B /\ ((B (_ A /\ y e. B) /\ x e. (A \ B))) -> -. x e. y)
38	37	adantll 309	. . . . . . . . . . . . . . . . . . . . 21 |- (((Ord A /\ Tr B) /\ ((B (_ A /\ y e. B) /\ x e. (A \ B))) -> -. x e. y)
39	22, 29, 38	ecased 643	. . . . . . . . . . . . . . . . . . . 20 |- (((Ord A /\ Tr B) /\ ((B (_ A /\ y e. B) /\ x e. (A \ B))) -> y e. x)
40	39	exp44 302	. . . . . . . . . . . . . . . . . . 19 |- ((Ord A /\ Tr B) -> (B (_ A -> (y e. B -> (x e. (A \ B) -> y e. x))))
41	40	com34 36	. . . . . . . . . . . . . . . . . 18 |- ((Ord A /\ Tr B) -> (B (_ A -> (x e. (A \ B) -> (y e. B -> y e. x))))
42	41	imp31 280	. . . . . . . . . . . . . . . . 17 |- ((((Ord A /\ Tr B) /\ B (_ A) /\ x e. (A \ B)) -> (y e. B -> y e. x))
43	42	ssrdv 1509	. . . . . . . . . . . . . . . 16 |- ((((Ord A /\ Tr B) /\ B (_ A) /\ x e. (A \ B)) -> B (_ x)
44	43	adantrr 312	. . . . . . . . . . . . . . 15 |- ((((Ord A /\ Tr B) /\ B (_ A) /\ (x e. (A \ B) /\ ((A \ B) i^i x) = (/))) -> B (_ x)
45	16, 44	eqssd 1518	. . . . . . . . . . . . . 14 |- ((((Ord A /\ Tr B) /\ B (_ A) /\ (x e. (A \ B) /\ ((A \ B) i^i x) = (/))) -> x = B)
46	9	ad2antrl 322	. . . . . . . . . . . . . 14 |- ((((Ord A /\ Tr B) /\ B (_ A) /\ (x e. (A \ B) /\ ((A \ B) i^i x) = (/))) -> x e. A)
47	45, 46	eqeltrrd 1164	. . . . . . . . . . . . 13 |- ((((Ord A /\ Tr B) /\ B (_ A) /\ (x e. (A \ B) /\ ((A \ B) i^i x) = (/))) -> B e. A)
48	47	exp32 294	. . . . . . . . . . . 12 |- (((Ord A /\ Tr B) /\ B (_ A) -> (x e. (A \ B) -> (((A \ B) i^i x) = (/) -> B e. A)))
49	48	r19.23adv 1286	. . . . . . . . . . 11 |- (((Ord A /\ Tr B) /\ B (_ A) -> (E.x e. (A \ B)((A \ B) i^i x) = (/) -> B e. A))
50		difss 1596	. . . . . . . . . . . 12 |- (A \ B) (_ A
51		tz7.5 2220	. . . . . . . . . . . 12 |- ((Ord A /\ ((A \ B) (_ A /\ -. (A \ B) = (/))) -> E.x e. (A \ B)((A \ B) i^i x) = (/))
52	50, 51	mpan21 531	. . . . . . . . . . 11 |- ((Ord A /\ -. (A \ B) = (/)) -> E.x e. (A \ B)((A \ B) i^i x) = (/))
53	49, 52	syl5 22	. . . . . . . . . 10 |- (((Ord A /\ Tr B) /\ B (_ A) -> ((Ord A /\ -. (A \ B) = (/)) -> B e. A))
54	53	exp4b 296	. . . . . . . . 9 |- ((Ord A /\ Tr B) -> (B (_ A -> (Ord A -> (-. (A \ B) = (/) -> B e. A))))
55	54	com23 32	. . . . . . . 8 |- ((Ord A /\ Tr B) -> (Ord A -> (B (_ A -> (-. (A \ B) = (/) -> B e. A))))
56	55	adantrd 308	. . . . . . 7 |- ((Ord A /\ Tr B) -> ((Ord A /\ Tr B) -> (B (_ A -> (-. (A \ B) = (/) -> B e. A))))
57	56	pm2.43i 58	. . . . . 6 |- ((Ord A /\ Tr B) -> (B (_ A -> (-. (A \ B) = (/) -> B e. A)))
58		pssdifn0 1750	. . . . . 6 |- ((B (_ A /\ -. B = A) -> -. (A \ B) = (/))
59	57, 58	syl7 24	. . . . 5 |- ((Ord A /\ Tr B) -> (B (_ A -> ((B (_ A /\ -. B = A) -> B e. A)))
60	59	exp4a 295	. . . 4 |- ((Ord A /\ Tr B) -> (B (_ A -> (B (_ A -> (-. B = A -> B e. A))))
61	60	pm2.43d 59	. . 3 |- ((Ord A /\ Tr B) -> (B (_ A -> (-. B = A -> B e. A)))
62	61	imp3a 279	. 2 |- ((Ord A /\ Tr B) -> ((B (_ A /\ -. B = A) -> B e. A))
63	7, 62	impbid 397	1 |- ((Ord A /\ Tr B) -> (B e. A <-> (B (_ A /\ -. B = A)))

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127   /\ wa 196   \/ w3o 580   = weq 797   e. wel 803   = wceq 1091   e. wcel 1092  E.wrex 1202   \ cdif 1484   i^i cin 1486   (_ wss 1487  (/)c0 1707  Tr wtr 2041  Ecep 2056   Fr wfr 2061   We wwe 2062  Ord word 2198

This theorem is referenced by:  ordelssne 2225

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202

metamath.org