Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem tz7.7 2224

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

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

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ↔ wb 127 ∧ wa 196 ∨ w3o 580 = weq 797 ∈ wel 803 = wceq 1091 ∈ wcel 1092 ∃wrex 1202 ∖ cdif 1484 ∩ 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