Theorem onint 3006

Description: The intersection (infimum) of a non-empty class of ordinal numbers belongs to the class. Compare Exercise 4 of [TakeutiZaring] p. 45.

Assertion

Ref	Expression
onint	|- ((A (_ On /\ A =/= (/)) -> |^|A e. A)

Proof of Theorem onint

Step	Hyp	Ref	Expression
1		ssel 2063	. . . . . . . . . . . . . . . . . . . 20 |- (A (_ On -> (z e. A -> z e. On))
2		ontri1 2981	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x e. On /\ z e. On) -> (x (_ z <-> -. z e. x))
3		ssel 2063	. . . . . . . . . . . . . . . . . . . . . 22 |- (x (_ z -> (y e. x -> y e. z))
4	2, 3	syl6bir 215	. . . . . . . . . . . . . . . . . . . . 21 |- ((x e. On /\ z e. On) -> (-. z e. x -> (y e. x -> y e. z)))
5	4	ex 373	. . . . . . . . . . . . . . . . . . . 20 |- (x e. On -> (z e. On -> (-. z e. x -> (y e. x -> y e. z))))
6	1, 5	sylan9 468	. . . . . . . . . . . . . . . . . . 19 |- ((A (_ On /\ x e. On) -> (z e. A -> (-. z e. x -> (y e. x -> y e. z))))
7	6	com4r 41	. . . . . . . . . . . . . . . . . 18 |- (y e. x -> ((A (_ On /\ x e. On) -> (z e. A -> (-. z e. x -> y e. z))))
8	7	imp31 362	. . . . . . . . . . . . . . . . 17 |- (((y e. x /\ (A (_ On /\ x e. On)) /\ z e. A) -> (-. z e. x -> y e. z))
9	8	r19.20dva 1709	. . . . . . . . . . . . . . . 16 |- ((y e. x /\ (A (_ On /\ x e. On)) -> (A.z e. A -. z e. x -> A.z e. A y e. z))
10		disj 2311	. . . . . . . . . . . . . . . 16 |- ((A i^i x) = (/) <-> A.z e. A -. z e. x)
11		visset 1813	. . . . . . . . . . . . . . . . 17 |- y e. V
12	11	elint2 2540	. . . . . . . . . . . . . . . 16 |- (y e. |^|A <-> A.z e. A y e. z)
13	9, 10, 12	3imtr4g 553	. . . . . . . . . . . . . . 15 |- ((y e. x /\ (A (_ On /\ x e. On)) -> ((A i^i x) = (/) -> y e. |^|A))
14		ssel 2063	. . . . . . . . . . . . . . . 16 |- (A (_ On -> (x e. A -> x e. On))
15	14	imdistani 443	. . . . . . . . . . . . . . 15 |- ((A (_ On /\ x e. A) -> (A (_ On /\ x e. On))
16	13, 15	sylan2 451	. . . . . . . . . . . . . 14 |- ((y e. x /\ (A (_ On /\ x e. A)) -> ((A i^i x) = (/) -> y e. |^|A))
17	16	exp32 377	. . . . . . . . . . . . 13 |- (y e. x -> (A (_ On -> (x e. A -> ((A i^i x) = (/) -> y e. |^|A))))
18	17	com4l 39	. . . . . . . . . . . 12 |- (A (_ On -> (x e. A -> ((A i^i x) = (/) -> (y e. x -> y e. |^|A))))
19	18	imp32 363	. . . . . . . . . . 11 |- ((A (_ On /\ (x e. A /\ (A i^i x) = (/))) -> (y e. x -> y e. |^|A))
20	19	ssrdv 2070	. . . . . . . . . 10 |- ((A (_ On /\ (x e. A /\ (A i^i x) = (/))) -> x (_ |^|A)
21		intss1 2548	. . . . . . . . . . 11 |- (x e. A -> |^|A (_ x)
22	21	ad2antrl 406	. . . . . . . . . 10 |- ((A (_ On /\ (x e. A /\ (A i^i x) = (/))) -> |^|A (_ x)
23	20, 22	eqssd 2079	. . . . . . . . 9 |- ((A (_ On /\ (x e. A /\ (A i^i x) = (/))) -> x = |^|A)
24	23	eleq1d 1540	. . . . . . . 8 |- ((A (_ On /\ (x e. A /\ (A i^i x) = (/))) -> (x e. A <-> |^|A e. A))
25	24	biimpd 153	. . . . . . 7 |- ((A (_ On /\ (x e. A /\ (A i^i x) = (/))) -> (x e. A -> |^|A e. A))
26	25	exp32 377	. . . . . 6 |- (A (_ On -> (x e. A -> ((A i^i x) = (/) -> (x e. A -> |^|A e. A))))
27	26	com34 36	. . . . 5 |- (A (_ On -> (x e. A -> (x e. A -> ((A i^i x) = (/) -> |^|A e. A))))
28	27	pm2.43d 65	. . . 4 |- (A (_ On -> (x e. A -> ((A i^i x) = (/) -> |^|A e. A)))
29	28	r19.23adv 1746	. . 3 |- (A (_ On -> (E.x e. A (A i^i x) = (/) -> |^|A e. A))
30		ordon 2987	. . . 4 |- Ord On
31		tz7.5 2969	. . . 4 |- ((Ord On /\ A (_ On /\ A =/= (/)) -> E.x e. A (A i^i x) = (/))
32	30, 31	mp3an1 903	. . 3 |- ((A (_ On /\ A =/= (/)) -> E.x e. A (A i^i x) = (/))
33	29, 32	syl5 21	. 2 |- (A (_ On -> ((A (_ On /\ A =/= (/)) -> |^|A e. A))
34	33	anabsi5 495	1 |- ((A (_ On /\ A =/= (/)) -> |^|A e. A)

Syntax hints:  -. wn 2   -> wi 3   /\ wa 223   = wceq 956   e. wcel 958   =/= wne 1585  A.wral 1645  E.wrex 1646   i^i cin 2046   (_ wss 2047  (/)c0 2280  |^|cint 2533  Ord word 2947  Oncon0 2948

This theorem is referenced by:  onint0 3007  onssmin 3008  onminsb 3009  onminesb 3010  oninton 3012  oneqmin 3018  onminex 3020  unblem1 4540  unblem2 4541  tz9.12lem3 4661  rankr1 4674  scott0 4717  oncardid 4821  cardid 4828  cardcf 4911

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779  ax-un 2866

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 776  df-3an 777  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-ral 1649  df-rex 1650  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-tp 2415  df-op 2416  df-uni 2504  df-int 2534  df-br 2620  df-opab 2667  df-tr 2681  df-eprel 2832  df-po 2840  df-so 2850  df-fr 2917  df-we 2934  df-ord 2951  df-on 2952

Copyright terms: Public domain