Metamath Proof Explorer


Theorem ltexprlem2

Description: Lemma for Proposition 9-3.5(iv) of Gleason p. 123. (Contributed by NM, 3-Apr-1996) (New usage is discouraged.)

Ref Expression
Hypothesis ltexprlem.1 C=x|y¬yAy+𝑸xB
Assertion ltexprlem2 B𝑷C𝑸

Proof

Step Hyp Ref Expression
1 ltexprlem.1 C=x|y¬yAy+𝑸xB
2 1 abeq2i xCy¬yAy+𝑸xB
3 elprnq B𝑷y+𝑸xBy+𝑸x𝑸
4 addnqf +𝑸:𝑸×𝑸𝑸
5 4 fdmi dom+𝑸=𝑸×𝑸
6 0nnq ¬𝑸
7 5 6 ndmovrcl y+𝑸x𝑸y𝑸x𝑸
8 3 7 syl B𝑷y+𝑸xBy𝑸x𝑸
9 ltaddnq x𝑸y𝑸x<𝑸x+𝑸y
10 9 ancoms y𝑸x𝑸x<𝑸x+𝑸y
11 addcomnq x+𝑸y=y+𝑸x
12 10 11 breqtrdi y𝑸x𝑸x<𝑸y+𝑸x
13 prcdnq B𝑷y+𝑸xBx<𝑸y+𝑸xxB
14 12 13 syl5 B𝑷y+𝑸xBy𝑸x𝑸xB
15 8 14 mpd B𝑷y+𝑸xBxB
16 15 ex B𝑷y+𝑸xBxB
17 16 adantld B𝑷¬yAy+𝑸xBxB
18 17 exlimdv B𝑷y¬yAy+𝑸xBxB
19 2 18 syl5bi B𝑷xCxB
20 19 ssrdv B𝑷CB
21 prpssnq B𝑷B𝑸
22 20 21 sspsstrd B𝑷C𝑸