Metamath Proof Explorer

Theorem ltexpri

Description: Proposition 9-3.5(iv) of Gleason p. 123. (Contributed by NM, 13-May-1996) (Revised by Mario Carneiro, 14-Jun-2013) (New usage is discouraged.)

Ref Expression
Assertion ltexpri ⊢A<𝑷B→∃x∈𝑷A+𝑷x=B

Proof

Step Hyp Ref Expression
1 ltrelpr ⊢<𝑷⊆𝑷×𝑷
2 1 brel ⊢A<𝑷B→A∈𝑷∧B∈𝑷
3 ltprord ⊢A∈𝑷∧B∈𝑷→A<𝑷B↔A⊂B
4 oveq2 ⊢y=z→w+𝑸y=w+𝑸z
5 4 eleq1d ⊢y=z→w+𝑸y∈B↔w+𝑸z∈B
6 5 anbi2d ⊢y=z→¬w∈A∧w+𝑸y∈B↔¬w∈A∧w+𝑸z∈B
7 6 exbidv ⊢y=z→∃w¬w∈A∧w+𝑸y∈B↔∃w¬w∈A∧w+𝑸z∈B
8 7 cbvabv ⊢y|∃w¬w∈A∧w+𝑸y∈B=z|∃w¬w∈A∧w+𝑸z∈B
9 8 ltexprlem5 ⊢B∈𝑷∧A⊂B→y|∃w¬w∈A∧w+𝑸y∈B∈𝑷
10 9 adantll ⊢A∈𝑷∧B∈𝑷∧A⊂B→y|∃w¬w∈A∧w+𝑸y∈B∈𝑷
11 8 ltexprlem6 ⊢A∈𝑷∧B∈𝑷∧A⊂B→A+𝑷y|∃w¬w∈A∧w+𝑸y∈B⊆B
12 8 ltexprlem7 ⊢A∈𝑷∧B∈𝑷∧A⊂B→B⊆A+𝑷y|∃w¬w∈A∧w+𝑸y∈B
13 11 12 eqssd ⊢A∈𝑷∧B∈𝑷∧A⊂B→A+𝑷y|∃w¬w∈A∧w+𝑸y∈B=B
14 oveq2 ⊢x=y|∃w¬w∈A∧w+𝑸y∈B→A+𝑷x=A+𝑷y|∃w¬w∈A∧w+𝑸y∈B
15 14 eqeq1d ⊢x=y|∃w¬w∈A∧w+𝑸y∈B→A+𝑷x=B↔A+𝑷y|∃w¬w∈A∧w+𝑸y∈B=B
16 15 rspcev ⊢y|∃w¬w∈A∧w+𝑸y∈B∈𝑷∧A+𝑷y|∃w¬w∈A∧w+𝑸y∈B=B→∃x∈𝑷A+𝑷x=B
17 10 13 16 syl2anc ⊢A∈𝑷∧B∈𝑷∧A⊂B→∃x∈𝑷A+𝑷x=B
18 17 ex ⊢A∈𝑷∧B∈𝑷→A⊂B→∃x∈𝑷A+𝑷x=B
19 3 18 sylbid ⊢A∈𝑷∧B∈𝑷→A<𝑷B→∃x∈𝑷A+𝑷x=B
20 2 19 mpcom ⊢A<𝑷B→∃x∈𝑷A+𝑷x=B