MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ordtbaslem Structured version   Visualization version   GIF version

Theorem ordtbaslem 23212
Description: Lemma for ordtbas 23216. In a total order, unbounded-above intervals are closed under intersection. (Contributed by Mario Carneiro, 3-Sep-2015.)
Hypotheses
Ref Expression
ordtval.1 𝑋 = dom 𝑅
ordtval.2 𝐴 = ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})
Assertion
Ref Expression
ordtbaslem (𝑅 ∈ TosetRel → (fi‘𝐴) = 𝐴)
Distinct variable groups:   𝑥,𝑦,𝑅   𝑥,𝑋,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)

Proof of Theorem ordtbaslem
Dummy variables 𝑎 𝑏 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 3anrot 1099 . . . . . . . . . . . . 13 ((𝑦𝑋𝑎𝑋𝑏𝑋) ↔ (𝑎𝑋𝑏𝑋𝑦𝑋))
2 ordtval.1 . . . . . . . . . . . . . 14 𝑋 = dom 𝑅
32tsrlemax 18644 . . . . . . . . . . . . 13 ((𝑅 ∈ TosetRel ∧ (𝑦𝑋𝑎𝑋𝑏𝑋)) → (𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (𝑦𝑅𝑎𝑦𝑅𝑏)))
41, 3sylan2br 595 . . . . . . . . . . . 12 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋𝑦𝑋)) → (𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (𝑦𝑅𝑎𝑦𝑅𝑏)))
543exp2 1353 . . . . . . . . . . 11 (𝑅 ∈ TosetRel → (𝑎𝑋 → (𝑏𝑋 → (𝑦𝑋 → (𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (𝑦𝑅𝑎𝑦𝑅𝑏))))))
65imp42 426 . . . . . . . . . 10 (((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) ∧ 𝑦𝑋) → (𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (𝑦𝑅𝑎𝑦𝑅𝑏)))
76notbid 318 . . . . . . . . 9 (((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) ∧ 𝑦𝑋) → (¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ ¬ (𝑦𝑅𝑎𝑦𝑅𝑏)))
8 ioran 985 . . . . . . . . 9 (¬ (𝑦𝑅𝑎𝑦𝑅𝑏) ↔ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏))
97, 8bitrdi 287 . . . . . . . 8 (((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) ∧ 𝑦𝑋) → (¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)))
109rabbidva 3440 . . . . . . 7 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} = {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)})
11 ifcl 4576 . . . . . . . . 9 ((𝑏𝑋𝑎𝑋) → if(𝑎𝑅𝑏, 𝑏, 𝑎) ∈ 𝑋)
1211ancoms 458 . . . . . . . 8 ((𝑎𝑋𝑏𝑋) → if(𝑎𝑅𝑏, 𝑏, 𝑎) ∈ 𝑋)
13 dmexg 7924 . . . . . . . . . . . 12 (𝑅 ∈ TosetRel → dom 𝑅 ∈ V)
142, 13eqeltrid 2843 . . . . . . . . . . 11 (𝑅 ∈ TosetRel → 𝑋 ∈ V)
1514adantr 480 . . . . . . . . . 10 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → 𝑋 ∈ V)
16 rabexg 5343 . . . . . . . . . 10 (𝑋 ∈ V → {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ V)
1715, 16syl 17 . . . . . . . . 9 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ V)
1810, 17eqeltrd 2839 . . . . . . . 8 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ V)
19 eqid 2735 . . . . . . . . . 10 (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}) = (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})
20 breq2 5152 . . . . . . . . . . . 12 (𝑥 = if(𝑎𝑅𝑏, 𝑏, 𝑎) → (𝑦𝑅𝑥𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)))
2120notbid 318 . . . . . . . . . . 11 (𝑥 = if(𝑎𝑅𝑏, 𝑏, 𝑎) → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)))
2221rabbidv 3441 . . . . . . . . . 10 (𝑥 = if(𝑎𝑅𝑏, 𝑏, 𝑎) → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} = {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)})
2319, 22elrnmpt1s 5973 . . . . . . . . 9 ((if(𝑎𝑅𝑏, 𝑏, 𝑎) ∈ 𝑋 ∧ {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ V) → {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}))
24 ordtval.2 . . . . . . . . 9 𝐴 = ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})
2523, 24eleqtrrdi 2850 . . . . . . . 8 ((if(𝑎𝑅𝑏, 𝑏, 𝑎) ∈ 𝑋 ∧ {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ V) → {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ 𝐴)
2612, 18, 25syl2an2 686 . . . . . . 7 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ 𝐴)
2710, 26eqeltrrd 2840 . . . . . 6 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴)
2827ralrimivva 3200 . . . . 5 (𝑅 ∈ TosetRel → ∀𝑎𝑋𝑏𝑋 {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴)
29 rabexg 5343 . . . . . . . 8 (𝑋 ∈ V → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ V)
3014, 29syl 17 . . . . . . 7 (𝑅 ∈ TosetRel → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ V)
3130ralrimivw 3148 . . . . . 6 (𝑅 ∈ TosetRel → ∀𝑎𝑋 {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ V)
32 breq2 5152 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝑦𝑅𝑥𝑦𝑅𝑎))
3332notbid 318 . . . . . . . . 9 (𝑥 = 𝑎 → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑦𝑅𝑎))
3433rabbidv 3441 . . . . . . . 8 (𝑥 = 𝑎 → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎})
3534cbvmptv 5261 . . . . . . 7 (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}) = (𝑎𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎})
36 ineq1 4221 . . . . . . . . . 10 (𝑧 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} → (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) = ({𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}))
37 inrab 4322 . . . . . . . . . 10 ({𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) = {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)}
3836, 37eqtrdi 2791 . . . . . . . . 9 (𝑧 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} → (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) = {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)})
3938eleq1d 2824 . . . . . . . 8 (𝑧 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} → ((𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴 ↔ {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴))
4039ralbidv 3176 . . . . . . 7 (𝑧 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} → (∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴 ↔ ∀𝑏𝑋 {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴))
4135, 40ralrnmptw 7114 . . . . . 6 (∀𝑎𝑋 {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ V → (∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴 ↔ ∀𝑎𝑋𝑏𝑋 {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴))
4231, 41syl 17 . . . . 5 (𝑅 ∈ TosetRel → (∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴 ↔ ∀𝑎𝑋𝑏𝑋 {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴))
4328, 42mpbird 257 . . . 4 (𝑅 ∈ TosetRel → ∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴)
44 rabexg 5343 . . . . . . . 8 (𝑋 ∈ V → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} ∈ V)
4514, 44syl 17 . . . . . . 7 (𝑅 ∈ TosetRel → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} ∈ V)
4645ralrimivw 3148 . . . . . 6 (𝑅 ∈ TosetRel → ∀𝑏𝑋 {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} ∈ V)
47 breq2 5152 . . . . . . . . . 10 (𝑥 = 𝑏 → (𝑦𝑅𝑥𝑦𝑅𝑏))
4847notbid 318 . . . . . . . . 9 (𝑥 = 𝑏 → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑦𝑅𝑏))
4948rabbidv 3441 . . . . . . . 8 (𝑥 = 𝑏 → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏})
5049cbvmptv 5261 . . . . . . 7 (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}) = (𝑏𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏})
51 ineq2 4222 . . . . . . . 8 (𝑤 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} → (𝑧𝑤) = (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}))
5251eleq1d 2824 . . . . . . 7 (𝑤 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} → ((𝑧𝑤) ∈ 𝐴 ↔ (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴))
5350, 52ralrnmptw 7114 . . . . . 6 (∀𝑏𝑋 {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} ∈ V → (∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴 ↔ ∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴))
5446, 53syl 17 . . . . 5 (𝑅 ∈ TosetRel → (∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴 ↔ ∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴))
5554ralbidv 3176 . . . 4 (𝑅 ∈ TosetRel → (∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴 ↔ ∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴))
5643, 55mpbird 257 . . 3 (𝑅 ∈ TosetRel → ∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴)
5724raleqi 3322 . . . 4 (∀𝑤𝐴 (𝑧𝑤) ∈ 𝐴 ↔ ∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴)
5824, 57raleqbii 3342 . . 3 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 ↔ ∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴)
5956, 58sylibr 234 . 2 (𝑅 ∈ TosetRel → ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)
6014pwexd 5385 . . . 4 (𝑅 ∈ TosetRel → 𝒫 𝑋 ∈ V)
61 ssrab2 4090 . . . . . . . 8 {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ⊆ 𝑋
6214adantr 480 . . . . . . . . 9 ((𝑅 ∈ TosetRel ∧ 𝑥𝑋) → 𝑋 ∈ V)
63 elpw2g 5339 . . . . . . . . 9 (𝑋 ∈ V → ({𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ 𝒫 𝑋 ↔ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ⊆ 𝑋))
6462, 63syl 17 . . . . . . . 8 ((𝑅 ∈ TosetRel ∧ 𝑥𝑋) → ({𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ 𝒫 𝑋 ↔ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ⊆ 𝑋))
6561, 64mpbiri 258 . . . . . . 7 ((𝑅 ∈ TosetRel ∧ 𝑥𝑋) → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ 𝒫 𝑋)
6665fmpttd 7135 . . . . . 6 (𝑅 ∈ TosetRel → (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}):𝑋⟶𝒫 𝑋)
6766frnd 6745 . . . . 5 (𝑅 ∈ TosetRel → ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}) ⊆ 𝒫 𝑋)
6824, 67eqsstrid 4044 . . . 4 (𝑅 ∈ TosetRel → 𝐴 ⊆ 𝒫 𝑋)
6960, 68ssexd 5330 . . 3 (𝑅 ∈ TosetRel → 𝐴 ∈ V)
70 inficl 9463 . . 3 (𝐴 ∈ V → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 ↔ (fi‘𝐴) = 𝐴))
7169, 70syl 17 . 2 (𝑅 ∈ TosetRel → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 ↔ (fi‘𝐴) = 𝐴))
7259, 71mpbid 232 1 (𝑅 ∈ TosetRel → (fi‘𝐴) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3a 1086   = wceq 1537  wcel 2106  wral 3059  {crab 3433  Vcvv 3478  cin 3962  wss 3963  ifcif 4531  𝒫 cpw 4605   class class class wbr 5148  cmpt 5231  dom cdm 5689  ran crn 5690  cfv 6563  ficfi 9448   TosetRel ctsr 18623
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-om 7888  df-1o 8505  df-2o 8506  df-en 8985  df-fin 8988  df-fi 9449  df-ps 18624  df-tsr 18625
This theorem is referenced by:  ordtbas2  23215
  Copyright terms: Public domain W3C validator